proposition: Lemma sum_nm_ext : forall (n m : nat) (f g : nat -> nat), (forall x : nat, x <= m -> f (n + x) = g (n + x)) -> sum_nm n m f = sum_nm n m g.
proof: Proof. intros n m; generalize n; clear n; elim m; simpl in |- *; auto. intros n f g H0; generalize (H0 0); rewrite Nat.add_comm; simpl in |- *; auto with arith. intros m' Rec n f g H0. rewrite (Rec (S n) f g). generalize (H0 0); rewrite Nat.add_comm; simpl in |- *; intros tmp; auto with arith. intros x H'; simpl in |- *; rewrite plus_n_Sm; auto with arith. Qed.
imports: Coq(Arith ArithRing)