rewrite < exp_plus_times.
apply eq_f.
rewrite > sym_plus.
- apply plus_minus_m_m.
- autobatch;
+ apply plus_minus_m_m.
+ autobatch by le_S_S_to_le, lt_mod_m_m, lt_O_S;
]
]
|intros.
change with ((i/S m) < S n).
apply (lt_times_to_lt_l m).
apply (le_to_lt_to_lt ? i);[2:assumption]
- apply eq_plus_to_le;[2:autobatch]
+ autobatch by eq_plus_to_le, div_mod, lt_O_S.
|apply le_exp
[assumption
|apply le_S_S_to_le.