+ [rewrite > H;rewrite > sym_times in ⊢ (? ? % ?);
+ rewrite > distr_times_plus in ⊢ (? ? % ?);
+ rewrite < minus_n_n in ⊢ (? ? ? (? (? (? ? (? ? %)) ?) ?));
+ rewrite > sym_times in ⊢ (? ? (? % ?) ?);
+ rewrite > sym_times in ⊢ (? ? (? ? %) ?);
+ rewrite > distributive_times_plus_sigma_p in ⊢ (? ? (? % ?) ?);
+ rewrite > distributive_times_plus_sigma_p in ⊢ (? ? (? ? %) ?);
+ rewrite > true_to_sigma_p_Sn in ⊢ (? ? (? ? %) ?)
+ [rewrite < assoc_plus;rewrite < sym_plus in ⊢ (? ? (? % ?) ?);
+ rewrite > assoc_plus;
+ apply eq_f2
+ [rewrite > sym_times;rewrite > assoc_times;autobatch paramodulation
+ |rewrite > (sigma_p_gi ? ? O);
+ [rewrite < (eq_sigma_p_gh ? S pred n1 (S n1) (λx:nat.true)) in ⊢ (? ? (? (? ? %) ?) ?)
+ [rewrite > (sigma_p_gi ? ? O) in ⊢ (? ? ? %);
+ [rewrite > assoc_plus;apply eq_f2
+ [autobatch paramodulation;
+ |rewrite < sigma_p_plus_1;
+ rewrite < (eq_sigma_p_gh ? S pred n1 (S n1) (λx:nat.true)) in \vdash (? ? ? %);
+ [apply eq_sigma_p
+ [intros;reflexivity
+ |intros;rewrite > sym_times;rewrite > assoc_times;
+ rewrite > sym_times in ⊢ (? ? (? (? ? %) ?) ?);
+ rewrite > assoc_times;rewrite < assoc_times in ⊢ (? ? (? (? ? %) ?) ?);
+ rewrite > sym_times in ⊢ (? ? (? (? ? (? % ?)) ?) ?);
+ change in ⊢ (? ? (? (? ? (? % ?)) ?) ?) with (exp a (S (n1 - S x)));
+ rewrite < (minus_Sn_m ? ? H1);rewrite > minus_S_S;
+ rewrite > sym_times in \vdash (? ? (? ? %) ?);
+ rewrite > assoc_times;
+ rewrite > sym_times in ⊢ (? ? (? ? (? ? %)) ?);
+ change in \vdash (? ? (? ? (? ? %)) ?) with (exp b (S x));
+ rewrite > assoc_times in \vdash (? ? (? ? %) ?);
+ rewrite > sym_times in \vdash (? ? (? % ?) ?);
+ rewrite > sym_times in \vdash (? ? (? ? %) ?);
+ rewrite > assoc_times in \vdash (? ? ? %);
+ rewrite > sym_times in \vdash (? ? ? %);
+ rewrite < distr_times_plus;
+ rewrite > sym_plus;rewrite < bc1;
+ [reflexivity|assumption]]
+ |intros;simplify;reflexivity
+ |intros;simplify;reflexivity
+ |intros;apply le_S_S;assumption
+ |intros;reflexivity
+ |intros 2;elim j
+ [simplify in H2;destruct H2
+ |simplify;reflexivity]
+ |intro;elim j
+ [simplify in H2;destruct H2
+ |simplify;apply le_S_S_to_le;assumption]]]
+ |apply le_S_S;apply le_O_n
+ |reflexivity]
+ |intros;simplify;reflexivity
+ |intros;simplify;reflexivity
+ |intros;apply le_S_S;assumption
+ |intros;reflexivity
+ |intros 2;elim j
+ [simplify in H2;destruct H2
+ |simplify;reflexivity]
+ |intro;elim j
+ [simplify in H2;destruct H2
+ |simplify;apply le_S_S_to_le;assumption]]
+ |apply le_S_S;apply le_O_n
+ |reflexivity]]
+ |reflexivity]
+ |reflexivity]]
+qed.
+
+theorem exp_S_sigma_p:\forall a,n.
+exp (S a) n = sigma_p (S n) (\lambda k.true) (\lambda k.(bc n k)*(exp a (n-k))).
+intros.
+rewrite > plus_n_SO.
+rewrite > exp_plus_sigma_p.
+apply eq_sigma_p;intros
+ [reflexivity
+ |rewrite < exp_SO_n.
+ rewrite < times_n_SO.
+ reflexivity
+ ]
+qed.
+
+theorem exp_Sn_SSO: \forall n. exp (S n) 2 = S((exp n 2) + 2*n).
+intros.simplify.
+rewrite < times_n_SO.
+rewrite < plus_n_O.
+rewrite < sym_times.simplify.
+rewrite < assoc_plus.
+rewrite < sym_plus.
+reflexivity.
+qed.
+