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

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

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

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

monotonic_lt_times_r : 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(c)(t)))))

Printing for OpenTheory is not working at the moment.