proposition: Lemma Rge_min_abs : forall x : R, x >= -Rabs x.
proof: Proof. intros. rewrite <- (Ropp_involutive x). apply Ropp_le_ge_contravar. rewrite (Rabs_Ropp (- x)). apply Rle_abs. Qed.
imports: Lra Coq.Reals.Reals Reals.ROrderedType Notations