fact: Definition XbinOp {R : ConstructiveReals} {X : Set} (f g : PartialFunction X) (op : CRcarrier R -> CRcarrier R -> CRcarrier R) (opEq : forall x y z t : CRcarrier R, x == y -> z == t -> op x z == op y t) : PartialFunction X := XbinOpXY X (CRcarrier R) (CReq R) f g op opEq.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete