proposition: Lemma nat_prime_p6 p p' n n': natp n -> natp n' -> nat_factor_list p n -> nat_factor_list p' n' -> oprodf p n = oprodf p' n' -> n = n' /\ same_below p p' n.
proof: Proof. move => nN n'N hn; move:n nN hn n' n'N; apply: Nat_induction. move => ha m mN hb eq1; case: (equal_or_not m \0c) => m0. by split => // i /clt0. move: (cpred_lt mN m0) => lt1. move:(nat_prime_p4 mN hb lt1); rewrite - eq1 oprod_f0 =>/(cdivides_oner). by move: (proj2 (proj32 (proj32 hb _ lt1)))=> bad eq2; case:bad. have aux : forall n, natp n -> forall q i, nat_factor_list q (csucc n) -> i <c csucc n -> q n <=o q i. move => n nN q i hyp /(cltSleP nN) /cle_eqVlt;case. by move ->; exact: (oleR (proj31 hyp _ (cltS nN))). move: n nN q i hyp; apply: Nat_induction; first by move => q i _ /clt0. move=> n nN Hrec q i hr /(cltSleP nN) /cle_eqVlt. have lt0 := (proj33 hr _ nN (cltS (NS_succ nN))). case => lin; first by rewrite lin. exact:(oleT lt0 (Hrec q i (nat_factor_list_rec (NS_succ nN) hr) lin)). move=> n nN Hrec nf1 m mN nf2 eq1. move:(nat_prime_p4 (NS_succ nN) nf1 (cltS nN)); rewrite eq1=> dvd1. have ppn:= (proj32 nf1 _ (cltS nN)). move:(nat_prime_p5 mN nf2 ppn dvd1) => [i lim ppni]. case: (equal_or_not m\0c) => mz; first by move:lim; rewrite mz => /clt0. move:(cpred_pr mN mz) => [m'N m'v]. move: (cpred_lt mN mz) => lt1. move:(nat_prime_p4 mN nf2 lt1); rewrite - eq1 => dvd2. have ppm:= (proj32 nf2 _ lt1). case: (equal_or_not (p' i) (p' (cpred m))) => he1. move: eq1. rewrite m'v in nf2 *. move: (nat_prime_factor_vS nN nf1) => [p1N f1N ->]. move: (nat_prime_factor_vS m'N nf2) => [p2N f2N ->]. rewrite - he1 - ppni => eq2. move: (nesym (proj2 (clt_ltT clt_01 (proj32 ppn)))) => pnz. move: (cprod_eq2r f1N p1N p2N pnz eq2)=> eq3. move: (nat_factor_list_rec nN nf1) (nat_factor_list_rec m'N nf2)=> nf1' nf2'. move: (Hrec nf1' _ m'N nf2' eq3) => [eq4 eq5]. split; [by rewrite eq4 | move => k /(cltSleP nN) lkn]. case:(cle_eqVlt lkn) => ltin; first by rewrite ltin ppni he1 eq4. by apply: eq5. move:(nat_prime_p5 (NS_succ nN) nf1 ppm dvd2) => [j ljn ppnj]. rewrite m'v in nf2 lim. have : p' (cpred m) <o p' i. split;[ exact: (aux _ m'N p' i nf2 lim) | exact: (nesym he1)]. rewrite ppnj - ppni => /oltNge; case; exact:(aux _ nN p j nf1 ljn). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)