proposition: Lemma Zge_opp : forall x y : Z, (x <= y)%Z -> (- x >= - y)%Z.
proof: Proof. intros. apply Z.le_ge. apply Zplus_le_reg_l with (p := (x + y)%Z). ring_simplify (x + y + - y)%Z (x + y + - x)%Z. assumption. Qed.
imports: Coq(Lia)