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. cut (- - a > - - (0))%Z. intro. cut (- a < - (0))%Z. simpl in |- *. intro. replace x with (- - x)%Z. replace y with (- - y)%Z. apply Zlt_opp. apply Zgt_mult_conv_absorb_l with (a := (- a)%Z) (x := (- x)%Z). assumption. rewrite Zmult_opp_opp. rewrite Zmult_opp_opp. assumption. apply Z.opp_involutive. apply Z.opp_involutive. apply Z.gt_lt. apply Zlt_opp. apply Z.gt_lt. assumption. simpl in |- *. rewrite Z.opp_involutive. assumption. Qed.
imports: Coq(Lia)