proposition: Lemma Nfinite_sum_split : forall n p q f, p + q = n -> Nfinite_sum_0_n (S n) f = Nfinite_sum_0_n p f + Nfinite_sum_0_n q (fun k => f (kth_S p k)).
proof: Proof. induction n. induction p. intros. simpl in H. rewrite H. unfold Nfinite_sum_0_n. unfold kth_S. auto with arith. intros. discriminate H. destruct p. intros. simpl in H. rewrite H. clear H. assert (Nfinite_sum_0_n 0 f=f 0). compute. reflexivity. rewrite H. clear H. rewrite Nfinite_sum_split_lower. unfold kth_S. reflexivity. intros. assert (p+q=n). auto with arith. clear H. assert (Nfinite_sum_0_n (S (S n)) f=f(S(S n))+Nfinite_sum_0_n (S n) f). rewrite Nat.add_comm. apply Nfinite_sum_split_upper. rewrite H. clear H. rewrite (IHn p q). rewrite Nfinite_sum_split_upper. assert (f (S p) + Nfinite_sum_0_n q (fun k : nat => f (kth_S (S p) k)) = Nfinite_sum_0_n (S q) (fun k=>f(kth_S p k))). rewrite Nfinite_sum_split_lower. rewrite kth_S_special. unfold kth_S. fold kth_S. assert (forall k:nat, kth_S p (S k)=S(kth_S p k)). intro. rewrite kth_S_sym. unfold kth_S. fold kth_S. rewrite kth_S_sym. reflexivity. assert (Nfinite_sum_0_n q (fun k : nat => f (S (kth_S p k)))= Nfinite_sum_0_n q (fun k : nat => f (kth_S p (S k)))). apply Nfinite_sum_eq_compat. intro. rewrite (H k). reflexivity. rewrite H1. reflexivity. assert (Nfinite_sum_0_n p f + f (S p) + Nfinite_sum_0_n q (fun k : nat => f (kth_S (S p) k)) = Nfinite_sum_0_n p f + (f (S p) + Nfinite_sum_0_n q (fun k : nat => f (kth_S (S p) k)))). auto with arith. rewrite H1. clear H1. rewrite H. clear H. assert (f (S (S n)) + (Nfinite_sum_0_n p f + Nfinite_sum_0_n q (fun k : nat => f (kth_S p k))) = Nfinite_sum_0_n p f + (Nfinite_sum_0_n q (fun k : nat => f (kth_S p k))+f (S (S n)))). rewrite Nat.add_comm. auto with arith. rewrite H. clear H. assert (Nfinite_sum_0_n (S q) (fun k : nat => f (kth_S p k)) = Nfinite_sum_0_n q (fun k : nat => f (kth_S p k)) + f (S (S n))). rewrite Nfinite_sum_split_upper. assert (kth_S p (S q)=S(S n)). rewrite kth_S_sym. unfold kth_S. fold kth_S. rewrite kth_S_sym. rewrite kth_S_plus. assert (q+p+1=(p+q)+1). auto with arith. rewrite H. rewrite H0. clear H. rewrite plus_1_r. reflexivity. rewrite <- H. reflexivity. rewrite H. auto with arith. exact H0. Qed.
imports: Arith Nk_ind Ndiv