proposition: Lemma ord_factor_unique p n p' n': ord_factor_list p n -> ord_factor_list p' n' -> oprodf p n = oprodf p' n' -> (n = n' /\ same_below p p' n).
proof: Proof. move => ha hb eq1. move:(ord_factor2 ha) => [k1 kb1]. move:(ord_factor2 hb) => [k2 kb2]. move:(ord_factor7 ha hb kb1 kb2 eq1) =>[k1k2]. set m := n -c k1; set m' := n' -c k1; rewrite - k1k2. set p1 := (fun i => p (i +c k1)); set p1' := (fun i => p' (i +c k1)). move => sb1 sp1 sp2 eq2. move:(ha)(hb) =>[nN ax1 ax2] [n'N ax1' ax2']. move:(proj31 kb1) => lenk1; move:(NS_le_nat lenk1 nN)=> k1N. move:(proj31 kb2) => lenk2. move: (cdiff_pr lenk1)=> k1v. have nax1: ofact_list_succ p1 m. have hi i: i <c m -> i +c k1 <c n. by move => likn; rewrite - k1v csumC; apply:(csum_Meqlt k1N). split; [ split | exact: sp1 ]. by apply: NS_diff. by move => i /hi lim; apply: ax1. move => i iN lim; move: (ax2 (i +c k1) (NS_sum iN k1N)). by rewrite /p1 (csum_Sn _ iN) -{1} (csum_Sn _ iN); apply; apply:hi. have nax2: ofact_list_succ p1' m'. move: (cdiff_pr lenk2)=> k2v. have hi i: i <c m' -> i +c k1 <c n'. by move => likn; rewrite - k2v csumC - k1k2; apply:(csum_Meqlt k1N). split; [ split | exact: sp2 ]. by apply: NS_diff. by move => i /hi lim; apply: ax1'. move => i iN lim; move: (ax2' (i +c k1) (NS_sum iN k1N)). by rewrite /p1' (csum_Sn _ iN) -{1} (csum_Sn _ iN); apply; apply:hi. move:(NS_diff k1 nN)(NS_diff k1 n'N) => mN mN'. move: (@ord_factor12 p1 m p1' m' nax1 nax2 eq2) =>[mm etc]; split. by rewrite - (cdiff_pr lenk1) - (cdiff_pr lenk2) - k1k2 -/m mm. move => i lin. case: (cleT_el (CS_nat k1N) (proj31_1 lin)); last by apply:sb1. move => ik1; move:(cdiff_pr ik1) => iv. move:(etc (i -c k1)); rewrite /p1/p1' csumC iv; apply. move:(NS_lt_nat lin nN) =>iN. by move:(csum_lt2l k1N (NS_diff k1 iN) mN); rewrite -/m iv k1v; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)