proposition: Lemma DiagNonNeg : forall {R : ConstructiveReals} {X : Set} (fnk : nat -> nat -> @PartialFunction R X), (forall n k:nat, nonNegFunc (fnk n k)) -> forall n:nat, nonNegFunc (diagSeq fnk n).
proof: Proof. intros. intros x xdf. unfold diagSeq. unfold diagSeq in xdf. destruct (diagPlaneInv n). apply H. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions