proposition: Lemma CReal_opp_gt_lt_contravar : forall r1 r2, r1 > r2 -> - r1 < - r2.
proof: Proof. unfold CRealGt; intros. apply (CReal_plus_lt_reg_l (r2 + r1)). rewrite CReal_plus_assoc, CReal_plus_opp_r, CReal_plus_0_r. rewrite CReal_plus_comm, <- CReal_plus_assoc, CReal_plus_opp_l. rewrite CReal_plus_0_l. exact H. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra