- rewrite > exp_S.
- rewrite > assoc_times in ⊢ (? ? %).
- apply le_times_r.
- rewrite > sym_times in ⊢ (? ? %).
- rewrite > assoc_times in ⊢ (? ? %).
- rewrite > assoc_times in ⊢ (? ? %).
- apply le_times_r.
- rewrite < assoc_times in ⊢ (? ? %).
- rewrite < assoc_times in ⊢ (? ? %).
- rewrite < sym_times in ⊢ (? ? (? (? % ?) ?)).
- rewrite > assoc_times in ⊢ (? ? %).
- rewrite > assoc_times in ⊢ (? ? %).
- apply le_times_r.
- rewrite > sym_times in ⊢ (? ? (? ? %)).
- rewrite > sym_times in ⊢ (? ? %).
- assumption
+ rewrite > S_pred in ⊢ (? ? (? (? ? %) ?))
+ [rewrite > exp_S.
+ rewrite > assoc_times in ⊢ (? ? %).
+ apply le_times_r.
+ rewrite > sym_times in ⊢ (? ? %).
+ rewrite > assoc_times in ⊢ (? ? %).
+ rewrite > assoc_times in ⊢ (? ? %).
+ apply le_times_r.
+ rewrite < assoc_times in ⊢ (? ? %).
+ rewrite < assoc_times in ⊢ (? ? %).
+ rewrite < sym_times in ⊢ (? ? (? (? % ?) ?)).
+ rewrite > assoc_times in ⊢ (? ? %).
+ rewrite > assoc_times in ⊢ (? ? %).
+ apply le_times_r.
+ rewrite > sym_times in ⊢ (? ? (? ? %)).
+ rewrite > sym_times in ⊢ (? ? %).
+ assumption
+ |unfold.rewrite > times_n_SO in ⊢ (? % ?).
+ apply le_times
+ [apply le_n_Sn
+ |assumption
+ ]
+ ]