proposition: Theorem sum_nm_split : forall (f : nat -> nat) (p q r : nat), r < q -> sum_nm p q f = sum_nm p r f + sum_nm (1 + (p + r)) (q - (1 + r)) f.
proof: Proof. intros f p q; elim q. intros r H; inversion H; simpl in |- *. intros n H r H0; inversion H0. rewrite sum_nm_f. rewrite Nat.sub_diag; rewrite <- plus_n_Sm; simpl in |- *; auto. rewrite sum_nm_f; rewrite (H r); auto with arith. rewrite Nat.sub_succ_l; auto with arith. rewrite sum_nm_f; auto with arith. replace (1 + (p + r) + S (n - (1 + r))) with (p + S n); auto with arith. rewrite <- Nat.sub_succ_l; auto with arith. replace (1 + (p + r) + (S n - (1 + r))) with (p + (1 + r + (S n - (1 + r)))); [ idtac | ring ]. simpl. rewrite <- (Nat.add_comm (n - r)). rewrite Nat.sub_add; auto with arith. Qed.
imports: Coq(Arith ArithRing)