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