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. case (dec_eq x y). intro. 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. case (not_Zeq x y H1). trivial. intro. 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(Lia)