∀ c, O < c ⇒ monotonic lt (λt. t × c)

Theorem monotonic_lt_times_l : forall (c:nat), (lt O c) -> relations.monotonic (nat) lt (fun (t:nat) => times t c).

theorem monotonic_lt_times_l : \forall (c:nat). ((lt) (O) c) -> (monotonic) (nat) (lt) (\lambda t : nat. (times) t c).

theorem monotonic_lt_times_l : forall (c:nat.nat) , ((((nat.lt_) ) ((nat.O) )) (c)) -> (((relations.monotonic) (nat.nat)) ((nat.lt_) )) (fun (t : nat.nat) , (((nat.times) ) (t)) (c)).

monotonic_lt_times_l : LEMMA (FORALL(c:nat_sttfa.sttfa_nat):(nat_sttfa.lt(nat_sttfa.sttfa_O)(c) => relations_sttfa_th.monotonic[nat_sttfa.sttfa_nat](nat_sttfa.lt)((LAMBDA(t:nat_sttfa.sttfa_nat):nat_sttfa.times(t)(c)))))

Printing for OpenTheory is not working at the moment.