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