proposition: Lemma Zle_reg_mult_l : forall x y a : Z, (0 < a)%Z -> (x <= y)%Z -> (a * x <= a * y)%Z.
proof: Proof. intros. apply Zplus_le_reg_l with (p := (- a * x)%Z). ring_simplify (- a * x + a * x)%Z. replace (- a * x + a * y)%Z with ((y - x) * a)%Z. apply Zmult_gt_0_le_0_compat. apply Z.lt_gt. assumption. unfold Zminus in |- *. apply Zle_left. assumption. ring. Qed.
imports: Coq(Lia)