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

Axiom

nat.decidable_le

Statement

∀ n m, decidable (n ≤ m)

Main Dependencies
Theory

Coq-Jumb
Statement

Theorem decidable_le : forall (n:nat), forall (m:nat), logic.decidable (le n m).



Matita-Jumb
Statement

theorem decidable_le : \forall (n:nat). \forall (m:nat). (decidable) ((le) n m).



Lean-jumb
Statement

theorem decidable_le : forall (n:nat.nat) , forall (m:nat.nat) , ((logic.decidable) ) ((((nat.le_) ) (n)) (m)).



PVS-jumb

Statement

decidable_le : LEMMA (FORALL(n:nat_sttfa.sttfa_nat):(FORALL(m:nat_sttfa.sttfa_nat):logic_sttfa_th.decidable(nat_sttfa.le(n)(m))))



OpenTheory

Printing for OpenTheory is not working at the moment.