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

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

theorem monotonic_le_plus_l : \forall (m:nat). (monotonic) (nat) (le) (\lambda n : nat. (plus) n m).

theorem monotonic_le_plus_l : forall (m:nat.nat) , (((relations.monotonic) (nat.nat)) ((nat.le_) )) (fun (n : nat.nat) , (((nat.plus) ) (n)) (m)).

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

Printing for OpenTheory is not working at the moment.