proposition: Lemma IntExtRightPos : forall {R : ConstructiveReals} {x y : CRcarrier R} (IntExt : @IntervalExtension R x y), x <= y -> 0 < y.
proof: Proof. intros. apply (CRlt_le_trans _ x). apply (CRlt_trans _ _ _ (fst (left_ordered IntExt)) (snd (left_ordered IntExt))). exact H. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia