proposition: Lemma IQR_mult_quot : forall q r : Q, Req_constr (IQR (q * r)) (IQR q * IQR r).
proof: Proof. intros. rewrite mult_IQR. apply Req_constr_refl. Qed.
imports: QArith_base Rdefinitions Raxioms ConstructiveReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveCauchyAbs ConstructiveRealsMorphisms