-cut (O < p)
- [rewrite < sigma_p2.
- apply (trans_eq ? ?
- (sigma_p (S n*S m) (\lambda x:nat.divides_b (x/S m) n)
- (\lambda x:nat.g (x/S m*(p)\sup(x\mod S m)))))
- [apply sym_eq.
- apply (eq_sigma_p_gh g ? (p_ord_inv p (S m)))
- [intros.
- lapply (divides_b_true_to_lt_O ? ? H H4).
- apply divides_to_divides_b_true
- [rewrite > (times_n_O O).
- apply lt_times
- [assumption
- |apply lt_O_exp.assumption
- ]
- |apply divides_times
- [apply divides_b_true_to_divides.assumption
- |apply (witness ? ? (p \sup (m-i \mod (S m)))).
- rewrite < exp_plus_times.
- apply eq_f.
- rewrite > sym_plus.
- apply plus_minus_m_m.
- autobatch
- ]
- ]
- |intros.
- lapply (divides_b_true_to_lt_O ? ? H H4).
- unfold p_ord_inv.
- rewrite > (p_ord_exp1 p ? (i \mod (S m)) (i/S m))
- [change with ((i/S m)*S m+i \mod S m=i).
- apply sym_eq.
- apply div_mod.
- apply lt_O_S
- |assumption
- |unfold Not.intro.
- apply H2.
- apply (trans_divides ? (i/ S m))
- [assumption|
- apply divides_b_true_to_divides;assumption]
- |apply sym_times.
- ]
- |intros.
- apply le_S_S.
- apply le_times
- [apply le_S_S_to_le.
- change with ((i/S m) < S n).
- apply (lt_times_to_lt_l m).
- apply (le_to_lt_to_lt ? i)
- [autobatch|assumption]
- |apply le_exp
- [assumption
- |apply le_S_S_to_le.
- apply lt_mod_m_m.
- apply lt_O_S
- ]
- ]
- |intros.
- cut (ord j p < S m)
- [rewrite > div_p_ord_inv
- [apply divides_to_divides_b_true
- [apply lt_O_ord_rem
- [elim H1.assumption
- |apply (divides_b_true_to_lt_O ? ? ? H4).
- rewrite > (times_n_O O).
- apply lt_times
- [assumption|apply lt_O_exp.assumption]
- ]
- |apply (divides_exp_to_divides_ord_rem ? m ? ? H H1 H2).
- apply divides_b_true_to_divides.
- assumption
- ]
- |assumption
- ]
- |apply (divides_exp_to_lt_ord ? ? ? ? H H1 H2).
- apply (divides_b_true_to_divides ? ? H4).
- apply (divides_b_true_to_lt_O ? ? H4)
- ]
- |intros.
- cut (ord j p < S m)
- [rewrite > div_p_ord_inv
- [rewrite > mod_p_ord_inv
- [rewrite > sym_times.
- apply sym_eq.
- apply exp_ord
- [elim H1.assumption
- |apply (divides_b_true_to_lt_O ? ? ? H4).
- rewrite > (times_n_O O).
- apply lt_times
- [assumption|apply lt_O_exp.assumption]
- ]
- |apply (divides_exp_to_lt_ord ? ? ? ? H H1 H2).
- apply (divides_b_true_to_divides ? ? H4).
- apply (divides_b_true_to_lt_O ? ? H4)
- ]
- |assumption
- ]
- |apply (divides_exp_to_lt_ord ? ? ? ? H H1 H2).
- apply (divides_b_true_to_divides ? ? H4).
- apply (divides_b_true_to_lt_O ? ? H4).
- ]
- |intros.
- rewrite > eq_p_ord_inv.
- rewrite > sym_plus.
- apply (lt_to_le_to_lt ? (S m +ord_rem j p*S m))
- [apply lt_plus_l.
- apply le_S_S.
- cut (m = ord (n*(p \sup m)) p)
- [rewrite > Hcut1.
- apply divides_to_le_ord
- [apply (divides_b_true_to_lt_O ? ? ? H4).
- rewrite > (times_n_O O).
- apply lt_times
- [assumption|apply lt_O_exp.assumption]
- |rewrite > (times_n_O O).
- apply lt_times
- [assumption|apply lt_O_exp.assumption]
- |assumption
- |apply divides_b_true_to_divides.
- assumption
- ]
- |unfold ord.
- rewrite > sym_times.
- rewrite > (p_ord_exp1 p ? m n)
- [reflexivity
- |assumption
- |assumption
- |reflexivity
- ]
- ]
- |change with (S (ord_rem j p)*S m \le S n*S m).
- apply le_times_l.
- apply le_S_S.
- apply divides_to_le
- [assumption
- |apply (divides_exp_to_divides_ord_rem ? m ? ? H H1 H2).
- apply divides_b_true_to_divides.
- assumption
- ]
- ]
- ]
- |apply eq_sigma_p
- [intros.
- elim (divides_b (x/S m) n);reflexivity
- |intros.reflexivity
- ]
- ]
- |elim H1.apply lt_to_le.assumption
- ]