proposition: Lemma diagSumMajTriangle : forall {R : ConstructiveReals} (u : nat -> nat -> CRcarrier R), (forall n k : nat, 0 <= u n k) -> forall n : nat, CRsum (diagSeq u) (diagPlane 0 n) <= CRsum (fun i => CRsum (u i) n) n.
proof: Proof. intros. rewrite diagSumTriangle. apply sum_Rle. intros. apply pos_sum_more. intros. apply H. apply Nat.le_sub_l. Qed.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits