proposition: Lemma Zmult_pos_mon_lt_lft : forall a b c : Z, (a > b)%Z -> (c > 0)%Z -> (c * a > c * b)%Z.
proof: Proof. intros a b c. induction c as [| p| p]. auto with zarith. intros Hab H0. induction p as [p Hrecp| p Hrecp| ]. 3: auto with zarith. replace (Zpos (xI p)) with (2 * Zpos p + 1)%Z by auto with zarith. repeat rewrite Zmult_plus_distr_l. cut (2 * Zpos p * a > 2 * Zpos p * b)%Z. auto with zarith. repeat rewrite <- Zmult_assoc. cut (Zpos p * a > Zpos p * b)%Z; auto with zarith. replace (Zpos (xO p)) with (2 * Zpos p)%Z by auto with zarith. repeat rewrite <- Zmult_assoc. cut (Zpos p * a > Zpos p * b)%Z; auto with zarith. intros Hab H0. inversion H0. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq(Lia)