proposition: Lemma Zmult_pos_mon_lt_rht : forall a b c : Z, (a > b)%Z -> (c > 0)%Z -> (a * c > b * c)%Z.
proof: Proof. intros a b c; rewrite (Zmult_comm a c); rewrite (Zmult_comm b c); apply Zmult_pos_mon_lt_lft. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq(Lia)