+ |apply divides_fact;
+ [apply (trans_le ? ? ? H1);apply leb_true_to_le;assumption
+ |apply lt_to_le;assumption]]
+ |apply le_log
+ [assumption
+ |cut (O = exp O n!)
+ [rewrite > Hcut;apply monotonic_exp1;constructor 2;
+ apply leb_true_to_le;assumption
+ |elim n
+ [reflexivity
+ |simplify;rewrite > exp_plus_times;rewrite < H6;
+ rewrite > sym_times;rewrite < times_n_O;reflexivity]]]]
+ |apply le_log
+ [assumption
+ |apply monotonic_exp1;apply leb_true_to_le;assumption]]
+ |rewrite > sym_plus;rewrite > sym_plus in \vdash (? ? %);apply le_minus_to_plus;
+ rewrite < minus_plus_m_m;apply H3;apply lt_to_le;assumption]
+ |assumption]
+ |lapply (not_le_to_lt ? ? (leb_false_to_not_le ? ? H5));
+ rewrite > eq_minus_n_m_O
+ [apply le_O_n
+ |apply le_log
+ [assumption
+ |apply monotonic_exp1;assumption]]]]
+qed.