proposition: Lemma ord_factor7 p n p' n' k k' (p1:= fun i => p (i +c k)) (p1':= fun i => p' (i +c k')): ord_factor_list p n -> ord_factor_list p' n' -> ord_factor_boundary p n k -> ord_factor_boundary p' n' k' -> oprodf p n = oprodf p' n' -> [/\ k = k', same_below p p' k, forall i, i <c n -c k -> osuccp (p1 i), forall i, i <c n' -c k -> osuccp (p1' i) & oprodf p1 (n -c k) = oprodf p1' (n' -c k)].
proof: Proof. move => fl fl' kp kp' eq1. move:(ord_factor6 fl kp); rewrite -/p1; move =>[ha hb hc hd [he hf hg]]. move:(ord_factor6 fl' kp'); rewrite -/p1'; move =>[ra rb rc rd [re rf rg]]. move:hf rf => [e1 oe1 e1v] [e2 oe2 e2v]. move: eq1; rewrite re he e1v e2v => eq2. move:(ovaluation7 oe1 oe2 hg rg eq2) => [eq3 ->]. have eq5: oprodf p k = oprodf p' k' by rewrite e1v e2v eq3. move:(ord_factor5 ha ra hc rc eq5) => [eq7 eq8]. by rewrite [k in n' -c k] eq7. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)