proposition: Lemma diagSumMajByLine : forall {R : ConstructiveReals} (u : nat -> nat -> CRcarrier R) (A : CRcarrier R), (forall n k : nat, 0 <= u n k) -> (forall n:nat, CRsum (diagSeq u) n <= A) -> forall n k:nat, CRsum (u n) k <= A.
proof: Proof. intros. specialize (H0 (diagPlane 0 (n + k))). rewrite diagSumTriangle in H0. apply (CRle_trans _ (CRsum (fun i : nat => CRsum (u i) (n + k - i)) (n + k))). pose proof (selectOneInSum (fun i : nat => CRsum (u i) (n + k - i)) (n + k) n). simpl in H1. rewrite Nat.add_comm in H1. rewrite Nat.add_sub in H1. rewrite Nat.add_comm in H1. apply H1. rewrite <- (Nat.add_0_r n). rewrite <- Nat.add_assoc. apply Nat.add_le_mono_l. apply Nat.le_0_l. intros. apply cond_pos_sum. intros. apply H. assumption. Qed.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits