proposition: Lemma CRmult_appart_reg_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R), 0 < r -> (r1 * r) ≶ (r2 * r) -> r1 ≶ r2.
proof: Proof. intros. destruct H0. - left. exact (CRmult_lt_reg_r r _ _ H c). - right. exact (CRmult_lt_reg_r r _ _ H c). Qed.
imports: QArith Qabs Qround