proposition: Lemma Rleft_inverse : forall r : R, (sum (r < IQR 0) (IQR 0 < r)) -> Req_constr (/ r * r) (IQR 1).
proof: Proof. intros. rewrite Rinv_l. - unfold IQR. rewrite <- R1_def. apply Req_constr_refl. - destruct H. + intro abs. subst r. unfold IQR in r0. rewrite <- R0_def in r0. apply (Rlt_asym _ _ r0 r0). + intro abs. subst r. unfold IQR in r0. rewrite <- R0_def in r0. apply (Rlt_asym _ _ r0 r0). Qed.
imports: QArith_base Rdefinitions Raxioms ConstructiveReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveCauchyAbs ConstructiveRealsMorphisms