∀ n m, decidable (n < m)

Theorem decidable_lt : forall (n:nat), forall (m:nat), logic.decidable (lt n m).

theorem decidable_lt : \forall (n:nat). \forall (m:nat). (decidable) ((lt) n m).

theorem decidable_lt : forall (n:nat.nat) , forall (m:nat.nat) , ((logic.decidable) ) ((((nat.lt_) ) (n)) (m)).

decidable_lt : LEMMA (FORALL(n:nat_sttfa.sttfa_nat):(FORALL(m:nat_sttfa.sttfa_nat):logic_sttfa_th.decidable(nat_sttfa.lt(n)(m))))

Printing for OpenTheory is not working at the moment.