// This prints the left floatting menu
Dedukti    Load Matita      Load Coq         Load Lean        Load PVS         Load OpenTheory Load
Dedukti-jumb

Theorem

nat.leb_elim

Statement

∀ n m P, n ≤ m ⇒ P true ⇒ ¬(n ≤ m) ⇒ P false ⇒ P (leb n m)

Main Dependencies
Theory

Coq-Jumb
Statement

Theorem leb_elim : forall (n:nat), forall (m:nat), forall (P:(bool.bool -> Prop)), ((le n m) -> P bool.true) -> ((connectives.Not (le n m)) -> P bool.false) -> P (leb n m).



Matita-Jumb
Statement

theorem leb_elim : \forall (n:nat). \forall (m:nat). \forall (P:bool -> Prop). (((le) n m) -> P (true) ) -> (((Not) ((le) n m)) -> P (false) ) -> P ((leb) n m).



Lean-jumb
Statement

theorem leb_elim : forall (n:nat.nat) , forall (m:nat.nat) , forall (P:(bool.bool) -> Prop) , (((((nat.le_) ) (n)) (m)) -> (P) ((bool.true) )) -> ((((connectives.Not) ) ((((nat.le_) ) (n)) (m))) -> (P) ((bool.false) )) -> (P) ((((nat.leb) ) (n)) (m)).



PVS-jumb

Statement

leb_elim : LEMMA (FORALL(n:nat_sttfa.sttfa_nat):(FORALL(m:nat_sttfa.sttfa_nat):(FORALL(P:[bool_sttfa_th.sttfa_bool -> bool]):((nat_sttfa.le(n)(m) => P(bool_sttfa_th.sttfa_true)) => ((connectives_sttfa_th.sttfa_Not(nat_sttfa.le(n)(m)) => P(bool_sttfa_th.sttfa_false)) => P(nat_sttfa.leb(n)(m)))))))



OpenTheory

Printing for OpenTheory is not working at the moment.