proposition: Lemma IQR_zero_quot : Req_constr (IQR 0) R0.
proof: Proof. unfold IQR. rewrite R0_def. apply Req_constr_refl. Qed.
imports: QArith_base Rdefinitions Raxioms ConstructiveReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveCauchyAbs ConstructiveRealsMorphisms