proposition: Lemma diagSumTriangle : forall {R : ConstructiveReals} (u : nat -> nat -> CRcarrier R), forall n : nat, CRsum (diagSeq u) (diagPlane 0 n) == CRsum (fun i => CRsum (u i) (n-i)) n.
proof: Proof. induction n. - simpl. unfold diagSeq. reflexivity. - assert (forall i:nat, i <= S n -> diagPlane 0 n + S i = diagPlane (S n - i) i)%nat. { intros. unfold diagPlane. rewrite Nat.add_0_l. rewrite Nat.sub_add. rewrite diagPlaneAbsNext. ring. assumption. } pose proof (H (S n)). rewrite Nat.sub_diag in H0. rewrite <- H0. assert (diagPlane 0 n + S (S n) = S (diagPlane 0 n) + (S n))%nat. ring. rewrite H1. rewrite sum_assoc. rewrite IHn. clear IHn. rewrite (reverse_sum (fun k : nat => diagSeq u (S (diagPlane 0 n) + k))). simpl. rewrite Nat.sub_diag. rewrite Nat.add_0_r. simpl. assert (diagSeq u (S (diagPlane 0 n)) = u (S n) O). { pose proof (H O (Nat.le_0_l (S n))). rewrite Nat.sub_0_r in H2. rewrite Nat.add_succ_r in H2. rewrite Nat.add_0_r in H2. rewrite H2. unfold diagSeq. rewrite diagPlaneInject. reflexivity. } rewrite H2. rewrite <- CRplus_assoc. apply CRplus_morph. rewrite <- sum_plus. apply CRsum_eq. intros. assert (match i with | 0 => S n | S l => n - l end = S (n - i))%nat. { destruct i. rewrite Nat.sub_0_r. reflexivity. rewrite Nat.sub_succ_r. rewrite Nat.succ_pred. reflexivity. apply Nat.sub_gt. assumption. } rewrite H4. simpl. apply CRplus_morph. reflexivity. pose proof (H (S (n - i))). simpl in H5. assert (S (n - i) <= S n)%nat. { apply le_n_S. apply Nat.le_sub_l. } 2: reflexivity. 2: apply Nat.le_refl. specialize (H5 H6). rewrite Nat.add_succ_r in H5. rewrite H5. unfold diagSeq. rewrite diagPlaneInject. rewrite sub_cancel_m. reflexivity. assumption. Qed.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits