proposition: Lemma diagSumMaj : forall {R : ConstructiveReals} (u : nat -> nat -> CRcarrier R) (A : CRcarrier R), (forall n k : nat, 0 <= u n k) -> (forall n k : nat, CRsum (fun i => CRsum (u i) k) n <= A) -> forall n:nat, CRsum (diagSeq u) n <= A.
proof: Proof. intros. destruct (diagPlaneInv n) as [i j] eqn:desN. apply (CRle_trans _ (CRsum (diagSeq u) (n+i))). - apply pos_sum_more. unfold diagSeq. intros. destruct (diagPlaneInv k). apply H. rewrite <- (Nat.add_0_r n). rewrite <- Nat.add_assoc. apply Nat.add_le_mono_l. rewrite Nat.add_0_l. apply Nat.le_0_l. - assert (diagPlane 0 (i+j) = n + i)%nat. pose proof (diagPlaneSurject n). rewrite desN in H1. unfold diagPlane in H1. unfold diagPlane. rewrite <- H1. simpl. ring. rewrite <- H1. apply (CRle_trans _ (CRsum (fun k => CRsum (u k) (i+j)) (i+j))). apply diagSumMajTriangle. apply H. apply H0. Qed.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits