proposition: Lemma Zgt_mult_conv_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. case (dec_eq x y). intro H1. apply False_ind. rewrite H1 in H0. cut ((a * y)%Z = (a * y)%Z). change ((a * y)%Z <> (a * y)%Z) in |- *. apply Zgt_not_eq. assumption. trivial. intro H1. case (not_Zeq x y H1). trivial. intro H2. apply False_ind. cut (a * y > a * x)%Z. apply Zgt_asym with (m := (a * y)%Z) (n := (a * x)%Z). assumption. apply Zlt_conv_mult_l. assumption. assumption. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)