proposition: Theorem mult_lt : forall a b c : nat, c <> 0 -> a < b -> a * c < b * c.
proof: Proof. intros a b c; elim c. intros H; elim H; auto. intros c'; case c'. intros; lia. intros c'' Hrec Hneq Hlt; repeat rewrite <- (fun x : nat => mult_n_Sm x (S c'')). lia. Qed.
imports: Coq(ArithRing) Coq(Compare_dec) Coq(Wf_nat) Coq(Arith) Coq(Lia)