proposition: Lemma Rinv_pos : forall r : R, (sum (r < IQR 0) (IQR 0 < r)) -> IQR 0 < r -> IQR 0 < / r.
proof: Proof. intros. rewrite Rlt_def. apply CRealLtForget. rewrite Rlt_def in H0. apply CRealLtEpsilon in H0. unfold IQR in H0. rewrite Rquot2 in H0. rewrite (Rrepr_inv r (inr H0)). unfold IQR. rewrite Rquot2. apply CReal_inv_0_lt_compat, H0. Qed.
imports: QArith_base Rdefinitions Raxioms ConstructiveReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveCauchyAbs ConstructiveRealsMorphisms