proposition: Lemma Zmin_cancel_Zle : forall x y : Z, (- x <= - y)%Z -> (y <= x)%Z.
proof: Proof. intros. apply Zmult_cancel_Zle with (a := (-1)%Z). constructor. replace (-1 * y)%Z with (- y)%Z. replace (-1 * x)%Z with (- x)%Z. assumption. ring. ring. Qed.
imports: Coq(Lia)