proposition: Lemma CReal_opp_ge_le_contravar : forall r1 r2, r1 >= r2 -> - r1 <= - r2.
proof: Proof. intros. intro abs. apply H. clear H. apply (CReal_plus_lt_reg_r (-r1-r2)). unfold CReal_minus. rewrite <- CReal_plus_assoc, CReal_plus_opp_r, CReal_plus_0_l. rewrite (CReal_plus_comm (-r1)), <- CReal_plus_assoc, CReal_plus_opp_r, CReal_plus_0_l. exact abs. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra