+lemma eq_p_max: \forall n,p,r:nat. O < n \to
+O < r \to
+r = (S O) \lor (max r (\lambda p:nat.eqb (r \mod (nth_prime p)) O)) < p \to
+p = max_prime_factor (r*(nth_prime p)\sup n).
+intros.
+apply sym_eq.
+unfold max_prime_factor.
+apply max_spec_to_max.
+split
+ [split
+ [rewrite > times_n_SO in \vdash (? % ?).
+ rewrite > sym_times.
+ apply le_times
+ [assumption
+ |apply lt_to_le.
+ apply (lt_to_le_to_lt ? (nth_prime p))
+ [apply lt_n_nth_prime_n
+ |rewrite > exp_n_SO in \vdash (? % ?).
+ apply le_exp
+ [apply lt_O_nth_prime_n
+ |assumption
+ ]
+ ]
+ ]
+ |apply eq_to_eqb_true.
+ apply divides_to_mod_O
+ [apply lt_O_nth_prime_n
+ |apply (lt_O_n_elim ? H).
+ intro.
+ apply (witness ? ? (r*(nth_prime p \sup m))).
+ rewrite < assoc_times.
+ rewrite < sym_times in \vdash (? ? ? (? % ?)).
+ rewrite > exp_n_SO in \vdash (? ? ? (? (? ? %) ?)).
+ rewrite > assoc_times.
+ rewrite < exp_plus_times.
+ reflexivity
+ ]
+ ]
+ |intros.
+ apply not_eq_to_eqb_false.
+ unfold Not.intro.
+ lapply (mod_O_to_divides ? ? ? H5)
+ [apply lt_O_nth_prime_n
+ |cut (Not (divides (nth_prime i) ((nth_prime p)\sup n)))
+ [elim H2
+ [rewrite > H6 in Hletin.
+ simplify in Hletin.
+ rewrite < plus_n_O in Hletin.
+ apply Hcut.assumption
+ |elim (divides_times_to_divides ? ? ? ? Hletin)
+ [apply (lt_to_not_le ? ? H3).
+ apply lt_to_le.
+ apply (le_to_lt_to_lt ? ? ? ? H6).
+ apply f_m_to_le_max
+ [apply (trans_le ? (nth_prime i))
+ [apply lt_to_le.
+ apply lt_n_nth_prime_n
+ |apply divides_to_le[assumption|assumption]
+ ]
+ |apply eq_to_eqb_true.
+ apply divides_to_mod_O
+ [apply lt_O_nth_prime_n|assumption]
+ ]
+ |apply prime_nth_prime
+ |apply Hcut.assumption
+ ]
+ ]
+ |unfold Not.intro.
+ apply (lt_to_not_eq ? ? H3).
+ apply sym_eq.
+ elim (prime_nth_prime p).
+ apply injective_nth_prime.
+ apply H8
+ [apply (divides_exp_to_divides ? ? ? ? H6).
+ apply prime_nth_prime.
+ |apply lt_SO_nth_prime_n
+ ]
+ ]
+ ]
+ ]
+qed.
+