proposition: Lemma nds_fL_prop3 i l f: inc f (permutations n) -> natp i -> natp l -> (csucc (csucc (i +c l))) <c n -> pL f i -> (forall j, j <=c l -> pS f (csucc (i+c j))) -> pL f (csucc (csucc (i +c l))) -> exists g, [/\ inc g (permutations n), nds_sc X n f = nds_sc X n g, forall j, j<c (csucc i) -> Vf f j = Vf g j & pL g (csucc i)].
proof: Proof. move => fp iN lN ltil2n p1 p2 p3. set i1:= csucc i; set il2:= csucc (csucc (i +c l)); set il3:= csucc il2. set il:= csucc (i +c l). rewrite -/il2 in ltil2n. have il1N:= NS_succ (NS_sum iN lN). have il2N:= (NS_lt_nat ltil2n nN). have il3N: inc il3 Nat by apply:NS_succ il2N. have i1N:= NS_succ iN. have i2N:= NS_succ i1N. have leil3n: il3 <=c n by apply/cleSltP. have lti1il2: i1 <c il2. rewrite /i1 /il2; apply:cltSS. exact (cle_ltT (Nsum_M0le l iN) (cltS (NS_sum iN lN))). have lti1n:=(clt_ltT lti1il2 ltil2n). have ltin:= (clt_ltT (cltS iN) lti1n). have Ha: inc il2 n by apply /(NltP nN). have Hb: inc i1 n by apply /(NltP nN). have le1:=(cleS (NS_succ iN)). move: (transposition_prop nN Ha Hb). set g := Lf _ _ _. move => [gp gssi gsi ngsi ggi]. move/permutationsP: (gp) => [[[fg _] _] sg tg]. move/permutationsP: (fp) => [[[ff _] _] sf tf]. set h:= f \co g. have fgP: f \coP g by split => //; ue. have pa: forall j, j <c csucc i -> Vf f j = Vf h j. move => j jsi. have jb: inc j n by apply /(NltP nN); exact : (clt_ltT jsi lti1n). have jb': inc j (source g) by ue. have ne1:= (proj2(clt_ltT jsi (lti1il2))). rewrite /h compfV//; rewrite ngsi //; exact (proj2 jsi). have pb: forall j, inc j n -> il3 <=c j -> Vf f j = Vf h j. move => j jsi l3. have jb': inc j (source g) by ue. have lt1:= (clt_leT (cltS il2N) l3). have ne2:= (nesym (proj2 (clt_ltT lti1il2 lt1))). have ne1:= nesym(proj2 lt1). by rewrite /h compfV // ngsi. have hp:= (permutation_Sc fp gp). have hh: pL h i1 by rewrite /h /pL compfV //; [ rewrite gsi | rewrite sg]. suff: nds_sc X n f = nds_sc X n h by exists h; split; exact. move: Xax => [[hw _] _ hu hv]. have ax: nds_ax X n by move => z /hw /proj32_1. move: (nds_ax_perm nN ax fp) (nds_ax_perm nN ax hp). rewrite /nds_sc. set Y:= (fun z => X (Vf f z)). set Z:= (fun z => X (Vf h z)); move => [aY _ ] [aZ _]. move: (cdiff_pr leil3n); set m := _ -c _ => mv. have mN: natp m by apply: (NS_diff _ nN). rewrite - mv in aY aZ |- *. rewrite (osum_fA il3N mN aY) (osum_fA il3N mN aZ). apply: f_equal2. apply: (osumf_exten mN) => z zm. have le2:il3 <=c z +c il3 by apply: csum_Mle0; fprops. have le3: inc (z +c il3) n. by apply/(NltP nN); rewrite - mv (csumC il3); apply:csum_Mlteq. by rewrite /Y/Z pb. set a := X (Vf f i); set b := X(Vf f i1); set c:= X(Vf f il2). have il2sg: inc il2 (source g) by ue. have i1sg: inc i1 (source g) by ue. have ib: inc i n by apply /(NltP nN). have ig: inc i (source g) by ue. rewrite 2! (osum_fS _ il2N). rewrite {1} /Z {1}/Y /h (compfV fgP il2sg) gssi -/b -/c. have le2: csucc (csucc i) <=c il2. apply/(cleSSP (CS_succ i) (CS_succ ((i +c l)))). apply/(cleSSP (CS_nat iN) (CS_sum2 i l)). apply: (Nsum_M0le _ iN). move: (cdiff_pr le2); set m1 := _ -c _ => m1v. have m1N: inc m1 Nat by apply: (NS_diff _ il2N). rewrite mv in aY aZ. have aY': nds_ax Y (csucc (csucc i) +c m1). move => z; rewrite m1v => l1; apply: aY; exact:(clt_ltT l1 ltil2n). have aZ': nds_ax Z (csucc (csucc i) +c m1). move => z; rewrite m1v => l1; apply: aZ; exact:(clt_ltT l1 ltil2n). have ha:= cltS iN. have hb:= (proj2 (clt_ltT ha lti1il2)). rewrite - m1v (osum_fA i2N m1N aY') (osum_fA i2N m1N aZ'). rewrite 2! (osum_fS _ i1N) 2! (osum_fS _ iN). rewrite {2 3} /Y {2 3} /Z /h (compfV fgP ig)(compfV fgP i1sg). rewrite gsi (ngsi _ ib hb (proj2 ha)) -/a -/b -/c. set A:= osumf _ m1. set B:= osumf _ i. have <-: A = (osumf (fun z => Z (z +c csucc (csucc i))) m1). apply: (osumf_exten m1N) => j lej. have [_ /nesym ltb]:i1 <c j +c csucc (csucc i). apply/(cleSltP i1N); apply:csum_Mle0; fprops. have lta: j +c csucc (csucc i) <c il2. rewrite - m1v (csumC _ m1); exact: (csum_Mlteq i2N lej). have hc: inc (j +c csucc (csucc i)) (source g). rewrite sg; apply/(NltP nN); rewrite - mv /il3 - m1v. rewrite (csum_Sn _ (NS_sum i2N m1N)) (csumC _ m1). apply: (clt_ltT lta); rewrite (csumC m1) m1v. apply /(cltSleP (NS_sum il2N mN)) /csum_M0le; fprops. by rewrite /Y/Z /h (compfV fgP hc) (ngsi _ _ (proj2 lta) ltb) // - sg. have <-: B = osumf Z i. apply: (osumf_exten iN) => j lej; rewrite /Y/Z pa //. exact: (clt_ltT lej ha). have oA: ordinalp A. apply: (OS_osumf m1N) => j jl1; apply: aY'. rewrite (csumC _ m1); exact:(csum_Mlteq i2N jl1). have oB: ordinalp B. apply: (OS_osumf iN) => j jl1; apply: aY; exact (clt_ltT jl1 ltin). have fis: Vf f i <c n by apply/(NltP nN); Wtac. have fil2s: Vf f il2 <c n by apply/(NltP nN); Wtac. have fi1s: Vf f i1 <c n by apply/(NltP nN); Wtac. have da:= (hv _ p1 fis). have dc:= (hv _ p3 fil2s); rewrite -/c in dc. move: (hu _(p2 _ (cle0n lN))). rewrite (csum0r (CS_nat iN)); rewrite -/b => db. have d1a: odegree b <o odegree a by ue. have d1c: odegree b <o odegree c by ue. move: (hw _ fis) (hw _ fil2s)(hw _ fi1s); rewrite -/a -/b -/c => ap cp bp. move: (proj32_1 ap)(proj32_1 bp)(proj32_1 cp) => oa ob oc. have hc: l +c (csucc (csucc i)) = il2. by rewrite csumC (csum_Sn _ i1N) (csum_Sn _ iN). have [eq1 eq2]: (A +o a = a /\ A +o c = c). have: m1 <=c l. apply:(csum_le2l i2N m1N lN). rewrite m1v (csumC _ l) hc; apply:cleR; fprops. rewrite /A; move:m1N; move:(m1); apply: Nat_induction. by move => _; rewrite osum_f0 (osum0l oa) (osum0l oc). move => q qN Hrec sql. have ql:= (cleT (cleS qN) sql). move:(Hrec ql) => [eqa eqb]. set d := (Y (q +c csucc (csucc i))). have oD: ordinalp (osumf (fun z => Y (z +c csucc (csucc i))) q). apply: (OS_osumf qN) => j jlt; apply:aY. have jlt1:=(clt_leT jlt ql). move:(csum_Mlteq i2N jlt1); rewrite hc => hd;apply:(clt_ltT hd ltil2n). have ql': q <c l by apply/(cleSltP qN). have lt2: q +c csucc (csucc i) <c n. move:(csum_Mlteq i2N ql'); rewrite hc => hd; exact(clt_ltT hd ltil2n). have lt3: Vf f (q +c csucc (csucc i)) <c k. have eq3: q +c (csucc (csucc i)) = csucc (i +c (csucc q)). rewrite (csum_nS _ i1N) csumC. by rewrite (csum_Sn _ iN) (csum_nS _ qN). by move: (p2 _ sql); rewrite - eq3. move: (hu _ lt3); rewrite -/(Y _ ) -/d => dd. have dp: \0o <o d. by apply: hw; apply /(NltP nN); Wtac; rewrite sf;apply /(NltP nN). have ot:= proj32_1 dp. have d2a: odegree d <o odegree a by ue. have d2c: odegree d <o odegree c by ue. rewrite !(osum_fS _ qN) - (osumA ot oD oa) eqa. rewrite - (osumA ot oD oc) eqb. by rewrite (ord_negl_p7 dp ap d2a)(ord_negl_p7 dp cp d2c). rewrite (osumA ob oa oB) (ord_negl_p7 bp ap d1a) (osumA oA oa oB) eq1. rewrite (osumA oc oa oB) (osumA oA (OS_sum2 oc oa) oB) (osumA oA oc oa) eq2. rewrite (osumA ob (OS_sum2 oc oa) oB)(osumA ob oc oa) (ord_negl_p7 bp cp d1c). done. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)