∀ n, monotonic lt (λm. m + n)

Theorem monotonic_lt_plus_l : forall (n:nat), relations.monotonic (nat) lt (fun (m:nat) => plus m n).

theorem monotonic_lt_plus_l : \forall (n:nat). (monotonic) (nat) (lt) (\lambda m : nat. (plus) m n).

theorem monotonic_lt_plus_l : forall (n:nat.nat) , (((relations.monotonic) (nat.nat)) ((nat.lt_) )) (fun (m : nat.nat) , (((nat.plus) ) (m)) (n)).

monotonic_lt_plus_l : LEMMA (FORALL(n:nat_sttfa.sttfa_nat):relations_sttfa_th.monotonic[nat_sttfa.sttfa_nat](nat_sttfa.lt)((LAMBDA(m:nat_sttfa.sttfa_nat):nat_sttfa.plus(m)(n))))

Printing for OpenTheory is not working at the moment.