proposition: Lemma Zgt_mult_reg_absorb_l : forall a x y : Z, (a > 0)%Z -> (a * x > a * y)%Z -> (x > y)%Z.
proof: Proof. intros a x y H H0. cut (- a < - (0))%Z. rewrite <- (Z.opp_involutive a) in H. rewrite <- (Z.opp_involutive 0) in H. simpl in |- *. intro H1. rewrite <- (Z.opp_involutive x). rewrite <- (Z.opp_involutive y). apply Zlt_opp. apply Zgt_mult_conv_absorb_l with (a := (- a)%Z) (x := (- x)%Z). assumption. rewrite Zopp_mult_distr_l_reverse. rewrite Zopp_mult_distr_l_reverse. apply Zlt_opp. rewrite <- Zopp_mult_distr_r. rewrite <- Zopp_mult_distr_r. apply Z.gt_lt. apply Zlt_opp. apply Z.gt_lt. assumption. lia. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)