proposition: Lemma Zmult_pos_mon : forall a b : Z, (a * b > 0)%Z -> (a * b >= a)%Z.
proof: Proof. intros a b. case a. auto with zarith. case b. auto with zarith. intros. set (pp := Zpos p0) in |- * at 2. rewrite <- (Zmult_1_l pp). unfold pp in |- *; clear pp. rewrite Zmult_comm. apply Zmult_pos_mon_le_rht. apply Zge_POS_1. apply Zge_POS_0. intros p q; simpl in |- *; intro H0; inversion H0. intros p H0. apply (Zge_trans (Zneg p * b) 0 (Zneg p)). auto with zarith. apply Zge_0_NEG. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq(Lia)