proposition: Lemma ord_factor5 p n p' n': ord_factor_list p n -> ord_factor_list p' n' -> (forall i, i <c n -> limit_ordinal (p i)) -> (forall i, i <c n' -> limit_ordinal (p' i)) -> oprodf p n = oprodf p' n' -> (n = n' /\ same_below p p' n).
proof: Proof. move => ha hb hc hd eq. move:(ord_factor4 ha hc) => [ra rb rc]. move:(ord_factor4 hb hd) =>[sa sb sc]. move: eq; rewrite rc sc. move:(proj31 ha)(proj31 hb) => nN nN'. move:(OS_CNFr0 nN rb) (OS_CNFr0 nN' sb). set u := CNFrv _ _; set v := CNFrv _ _=> ou ov eq2. case: (oleT_ell ou ov); last first. - move/opow_Mo_lt => /proj2; case; symmetry; done. - by move/opow_Mo_lt => /proj2; case. - move => eq3. move:(CNFr_unique rb sb nN nN' eq3)=> [eq1 eq5]; split; first exact. rewrite - eq1 in sa. move => i lin; rewrite (ra _ lin) (sa _ lin). move:(cdiff_lt_symmetry nN lin) => he. have hf: (cpred (n -c cpred (n -c i))) = i. have iN := (NS_lt_nat lin nN). have hf: csucc i <=c n by apply/(cleSltP iN). by rewrite (cdiff_A1 nN iN hf) (double_diff nN hf) (cpred_pr2 iN). by move: (eq5 (cpred (n -c i)) he); rewrite - (eq1) hf => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)