proposition: Lemma inv_sum_nm : forall (P : nat -> Prop) (n i : nat) (f : nat -> nat), (forall a b : nat, P a -> P b -> P (a + b)) -> (forall x : nat, x <= i -> P (f (n + x))) -> P (sum_nm n i f).
proof: Proof. intros P n i f; generalize n; clear n; elim i; simpl in |- *; auto. intros n H H0; generalize (H0 0); rewrite Nat.add_comm; simpl in |- *; auto with arith. intros i' Rec n Pi Hx. apply Pi; auto. generalize (Hx 0); rewrite Nat.add_comm; simpl in |- *; intros tmp; auto with arith. apply Rec; auto. intros x H'; simpl in |- *; rewrite plus_n_Sm; auto with arith. Qed.
imports: Coq(Arith ArithRing)