proposition: Lemma Zmult_cancel_Zle : forall a x y : Z, (a < 0)%Z -> (a * x <= a * y)%Z -> (y <= x)%Z.
proof: Proof. intros. case (Z_le_gt_dec y x). trivial. intro. apply False_ind. apply (Z.lt_irrefl (a * x)). apply Z.le_lt_trans with (m := (a * y)%Z). assumption. apply Z.gt_lt. apply Zlt_conv_mult_l. assumption. apply Z.gt_lt. assumption. Qed.
imports: Coq(Lia)