proposition: Lemma zeroNonNeg : forall {R : ConstructiveReals}, nonNegFunc (@Xconst R (CRcarrier R) 0).
proof: Proof. intros R x xdf. apply CRle_refl. Qed.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete