proposition: Lemma CRopp_ge_le_contravar : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R), r2 <= r1 -> - r1 <= - r2.
proof: Proof. intros. intros abs. apply CRopp_lt_cancel in abs. contradiction. Qed.
imports: QArith Qabs Qround