nat.decidable_le
∀ n m, decidable (n ≤ m)
Theorem decidable_le : forall (n:nat), forall (m:nat), logic.decidable (le n m).
theorem decidable_le : \forall (n:nat). \forall (m:nat). (decidable) ((le) n m).
theorem decidable_le : forall (n:nat.nat) , forall (m:nat.nat) , ((logic.decidable) ) ((((nat.le_) ) (n)) (m)).
decidable_le : LEMMA (FORALL(n:nat_sttfa.sttfa_nat):(FORALL(m:nat_sttfa.sttfa_nat):logic_sttfa_th.decidable(nat_sttfa.le(n)(m))))
Printing for OpenTheory is not working at the moment.