proposition: Lemma ord_factor12 p n p' n': ofact_list_succ p n -> ofact_list_succ p' n' -> oprodf p n = oprodf p' n' -> (n = n' /\ same_below p p' n).
proof: Proof. move => ha. have nN:= (proj31 (proj1 ha)). move: (cleR (CS_nat nN)) => lnn; move: n nN p {-2} n p' n' lnn ha (nN). have H0 p n: ofact_list_succ p n -> ord_below p n. by move/proj1/ ord_factor1. have H1 p n: ofact_list_succ p n -> oprodf p n = \1o -> n = \0c. move => Ha;move: (Ha) =>[[nN ax1 _] _]. case: (equal_or_not n \0c) => // np. move:(cpred_pr nN np) => [mN mv]; rewrite mv (oprod_fS _ mN). move:(H0 _ _ Ha); rewrite {1}mv => /(true_below_rec mN) [oo1 oo2]. move/(oprod2_one (OS_oprodf mN oo1) oo2) =>[_ sf1]. by move: (ax1 _ (cpred_lt nN np)) => [_ /proj2]; case. have H2 p k n: ofact_list_succ p (k +c n) -> natp k -> natp n -> ofact_list_succ (fun i => p (i +c k)) n. move => [[_ ax1 ax2] ax3] kN nN; split. split; first exact. by move => i lin; apply: ax1; rewrite csumC; apply: csum_Meqlt. move => i iN lin; rewrite (csum_Sn _ iN); apply: ax2; first fprops. by rewrite -(csum_Sn _ iN) csumC; apply: csum_Meqlt. by move => i lin; apply: ax3; rewrite csumC; apply: csum_Meqlt. apply: Nat_induction. move => p n p' n' /cle0 -> _ _ osp /esym. by rewrite oprod_f0 => eq1; move:(H1 _ _ osp eq1) ->; split => // i /clt0. move => B BN Hrec p n p' n';case/ cle_eqVlt => lnB; last first. move/(cltSleP BN): lnB; apply:Hrec. move => ofl1 nN ofl2 eq1. move:(ord_factor11 ofl1) => [ec1 [m1 [mn1 ax1 prod1 em1]]]. move:(ord_factor11 ofl2) => [ec2 [m2 [mn2 ax2 prod2 em2]]]. have eq2: CNFpv ec1 m1 = CNFpv ec2 m2 by rewrite- prod1 - prod2. move: (CNFp_unique ax1 ax2 mn1 mn2 eq2) => [res1 res2]. move:(f_equal Q (res2 _ (cltS mn1))); rewrite em1 res1 em2; aw. have n'N := proj31 (proj1 ofl2). move:(first_non_int_p1 p nN) (first_non_int_p1 p' n'N). set k1 :=(first_non_int p n); set k2 := (first_non_int p' n'). move =>[k11 k12][k21 k22] eq3. have lk1n: k1 <=c n. by case: k11; [ by move ->; apply: (cleR (CS_nat nN)) | case;case]. have lk2n: k2 <=c n'. by case: k21; [ by move ->; apply: (cleR (CS_nat n'N)) | case;case]. move:(NS_le_nat lk1n nN)(NS_le_nat lk2n n'N) => k1N k2N. have nf1: nat_factor_list p k1. have hu i: i <c k1 -> (p i) <o omega0 by move/k12/olt_omegaP. move:(H0 _ _ ofl1)=> pax4;move:ofl1 => [[_ pax1 pax2] pax3]; split. - by move => i lik; move:(pax4 _ (clt_leT lik lk1n)) => pi. - move => i lik; move:(pax1 _ (clt_leT lik lk1n)) => pi. move:(oltNge(hu _ lik)) => npi. case/ord_prime_p1:pi; first exact. - move/ord_ptypeI_prop => [_ /npi]; case. - move/ord_ptypeL_prop => [_ /npi]; case. - move => i iN lik; move:(hu _ lik) (hu _ (clt_ltT (cltS iN) lik)) => f1 f2. exact:(proj1 (pax2 _ iN (clt_leT lik lk1n)) f2 f1). have nf2: nat_factor_list p' k2. have hu i: i <c k2 -> (p' i) <o omega0 by move/k22/olt_omegaP. move:(H0 _ _ ofl2)=> pax4;move:ofl2 => [[_ pax1 pax2] pax3]; split. - move => i lik; exact:(pax4 _ (clt_leT lik lk2n)). - move => i lik; move:(pax1 _ (clt_leT lik lk2n)) => pi. move:(oltNge(hu _ lik)) => npi. case/ord_prime_p1:pi; first exact. - move/ord_ptypeI_prop => [_ /npi]; case. - move/ord_ptypeL_prop => [_ /npi]; case. - move => i iN lik; move:(hu _ lik) (hu _ (clt_ltT (cltS iN) lik)) => f1 f2. exact:(proj1 (pax2 _ iN (clt_leT lik lk2n)) f2 f1). move:(@nat_prime_p6 p p' k1 k2 k1N k2N nf1 nf2 eq3) => [k1k2 sbk]. case: (equal_or_not k1 \0c) => k1nz; last first. move:(cdiff_pr lk1n); move:(NS_diff k1 nN); set n1 := n -c k1. move:(cdiff_pr lk2n); move:(NS_diff k2 n'N); set n2 := n' -c k2. move => n2N n'v n1N nv. move: (H0 _ _ ofl1) (H0 _ _ ofl2); rewrite - nv -n'v => cax1 cax2. move/posnat_ordinalp:(proj33(proj2 ax1)); rewrite em1 -/k1; aw => fcp. move: eq1; rewrite -nv -n'v (oprod_fA k1N n1N cax1)(oprod_fA k2N n2N cax2). rewrite - eq3. set p1 := fun i => p (i +c k1);set p2 := fun i => p' (i +c k2). have oo1: ordinalp (oprodf p1 n1). apply:(OS_oprodf n1N) => i lin. by apply:cax1; rewrite csumC; apply:(csum_Meqlt k1N lin). have oo2: ordinalp (oprodf p2 n2). apply:(OS_oprodf n2N) => i lin. by apply:cax2; rewrite csumC; apply:(csum_Meqlt k2N lin). move/(oprod2_simpl oo1 oo2 (proj1 fcp)) => eq4. have aux1: n1 <=c B. by apply/(cltSleP BN); rewrite - lnB - nv csumC; apply:csum_M0lt. rewrite -nv in ofl1; move: (H2 _ _ _ ofl1 k1N n1N)=> aux2. rewrite -n'v in ofl2; move: (H2 _ _ _ ofl2 k2N n2N)=> aux3. move:(Hrec p1 n1 p2 n2 aux1 aux2 n1N aux3 eq4)=> [n1n2 eq5]; split. by rewrite k1k2 n1n2. move => i lik; case:(cleT_el (CS_nat k1N) (proj31_1 lik)); last first. apply: sbk. move => kli; move:(cdiff_pr kli) => iv. move: (eq5 (i -c k1)); rewrite /p1 /p2 - k1k2 csumC iv; apply. have iN := (NS_lt_nat lik (NS_sum k1N n1N)). by apply:(csum_lt2l k1N (NS_diff k1 iN) n1N); rewrite iv. move:k11; rewrite k1nz;case => nz. move/esym: eq1;rewrite -nz oprod_f0 => eq1. by move:(H1 _ _ ofl2 eq1) ->; clear; split => // i /clt0. move:k21; rewrite -k1k2 k1nz;case => nz'. move:eq1;rewrite - nz' oprod_f0 => eq1. by move:(H1 _ _ ofl1 eq1) ->; clear; split => // i /clt0. clear k1 k2 k1N k2N k12 k22 eq3 lk1n lk2n nf1 nf2 k1k2 sbk k1nz. clear mn1 ax1 prod1 em1 mn2 ax2 prod2 em2 eq2 res1 res2. clear ec1 ec2 m1 m2. move:nz nz' => [/proj2 /nesym nz pnz] [/proj2 /nesym nz' pnz']. move:(cpred_pr nN nz) (cpred_pr n'N nz'). set m1 := (cpred n); set m2 := (cpred n'). move => [m1N nv][m2N nv']. rewrite nv in ofl1 eq1; rewrite nv' in ofl2 eq1. move:(ord_factor10 ofl1 m1N pnz) (ord_factor10 ofl2 m2N pnz'). move => [ec1 [q1 [q1N ax1 f1v [_ _ e10]]]]. move => [ec2 [q2 [q2N ax2 f2v [_ _ e20]]]]. move: (eq1); rewrite f1v f2v => eq2. move:(CNFp_unique ax1 ax2 (NS_succ q1N) (NS_succ q2N) eq2)=> [_ e1e2]. move: (f_equal P (e1e2 _ (succ_positive (csucc q1)))). rewrite e10 e20 => eqa. clear ec1 ec2 q1 q1N ax1 f1v e10 q2N ax2 f2v e20 eq2 e1e2. case:(ord_factor8 ofl1 (succ_positive m1));first by move=> [pp _ _]; case: pnz. case:(ord_factor8 ofl2 (succ_positive m2));first by move=> [pp _ _]; case: pnz'. move => [op01 _ p0v1] [op02 _ p0v2]. have eq2: p\0c = p' \0c by rewrite p0v1 p0v2 eqa. move:(Nsucc_rw m1N); rewrite csumC => m1v. move:(Nsucc_rw m2N); rewrite csumC => m2v. move: eq1. rewrite (oprod_f1r (H0 _ _ ofl1) m1N) (oprod_f1r (H0 _ _ ofl2) m2N) - eq2. rewrite m1v in ofl1; rewrite m2v in ofl2. move: (H2 _ _ _ ofl1 NS1 m1N)(H2 _ _ _ ofl2 NS1 m2N). set p1 := (fun i => p (i +c \1c)); set p1' := (fun i => p' (i +c \1c)). move => ofl1' ofl2'. have ->: oprodf (fun i => p (csucc i)) m1 = oprodf p1 m1. apply: (oprodf_exten m1N) => i lin. by rewrite /p1 (Nsucc_rw (NS_lt_nat lin m1N)). have ->: oprodf (fun i => p' (csucc i)) m2 = oprodf p1' m2. apply: (oprodf_exten m2N) => i lin. by rewrite /p1 (Nsucc_rw (NS_lt_nat lin m2N)). move:(OS_oprodf m1N (H0 _ _ ofl1'))=> op1. move:(OS_oprodf m2N (H0 _ _ ofl2'))=> op2 eq3. have cp: \0o <o (p \0c). apply:(ord_ne0_pos op02); rewrite p0v2; apply:osucc_nz. move:(oprod2_simpl op1 op2 cp eq3) => eq4. have lm1b: m1 <=c B. move: nv; rewrite lnB => ss; move:(CS_nat BN) (CS_nat m1N) => c1 c2. rewrite (csucc_inj c1 c2 ss); apply:(cleR c2). move:(Hrec p1 m1 p1' m2 lm1b ofl1' m1N ofl2' eq4) =>[m1m2 etc]; split. by rewrite nv nv' m1m2. rewrite nv => i lin; case: (equal_or_not i \0c)=> eiz; first by rewrite eiz. move:(cpred_pr (NS_lt_nat lin (NS_succ m1N)) eiz) => [ha hb]. have hc: cpred i <c m1 by apply/(cltSSP(CS_nat ha) (CS_nat m1N)); rewrite - hb. by move:(etc (cpred i) hc); rewrite /p1 /p1' -(Nsucc_rw ha) - hb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)