+ [ O \Rightarrow f m
+ | (S p) \Rightarrow (f (S p+m))*(pi p f m)].
+
+theorem eq_sigma: \forall f,g:nat \to nat.
+\forall n,m:nat.
+(\forall i:nat. m \le i \to i \le m+n \to f i = g i) \to
+(sigma n f m) = (sigma n g m).
+intros 3.elim n.
+simplify.apply H.apply le_n.rewrite < plus_n_O.apply le_n.
+simplify.
+apply eq_f2.apply H1.
+change with m \le (S n1)+m.apply le_plus_n.
+rewrite > sym_plus m.apply le_n.
+apply H.intros.apply H1.assumption.
+rewrite < plus_n_Sm.
+apply le_S.assumption.
+qed.