proposition: Lemma Req_constr_refl : forall x:R, Req_constr x x.
proof: Proof. split. - intro H. exact (Rlt_asym _ _ H H). - intro H. exact (Rlt_asym _ _ H H). Qed.
imports: QArith_base Rdefinitions Raxioms ConstructiveReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveCauchyAbs ConstructiveRealsMorphisms