proposition: Lemma expansion_prop12 f g b kf kg l n: n <=c kf -> n <=c kg -> l <c n -> (forall i, n <=c i -> i <c kf -> Vg f i = \0c) -> (forall i, n <=c i -> i <c kg -> Vg g i = \0c) -> (forall i, l <c i -> i <c n -> Vg f i = Vg g i) -> expansion f b kf -> expansion g b kg -> (Vg f l) <c (Vg g l) -> (expansion_value f b) <c (expansion_value g b).
proof: Proof. move=> nkf nkg ln pf pg pfg ef eg vl. move: (expansion_restr1 ef nkf). rewrite -(expansion_restr2 ef nkf pf). move: (expansion_restr1 eg nkg). rewrite -(expansion_restr2 eg nkg pg). set F := (restr f n). set G := (restr g n). move=> eG eF; clear pf pg. move: (ef) => [bN kfN _ [fgf df vf]]. move: (eg) => [_ kgN b2 [fgg dg vg]]. have nN:= NS_le_nat nkf kfN. have lN:= NS_lt_nat ln nN. have pFG: forall i, l <c i -> i <c n -> Vg F i = Vg G i. move=> i i1 i2; move: (pfg _ i1 i2). have ii: inc i n by apply /NltP. by rewrite /F/G !LgV //. have vL: (Vg F l) <c (Vg G l). have ii: inc l n by apply /NltP. by rewrite /F/G !LgV. clear pfg vl ef eg fgg fgf df dg vf vg. set fi := fun i => expansion_value (restr F i) b. set gi := fun i => expansion_value (restr G i) b. move: (eF) (eG) => [_ _ _ [fgf df vf]] [_ _ _ [fgg dg vg]]. have <-: (fi n = expansion_value F b) by rewrite /fi -df restr_to_domain. have <-: (gi n = expansion_value G b) by rewrite /gi -dg restr_to_domain. pose r i := (fi i) <c (gi i). have cl2: natp (csucc l) by fprops. have cl0: (csucc l) <=c n by apply /cleSltP. apply: (Nat_induction3 (r:=r) cl2 nN _ _ cl0 (cleR (proj31 nkf))). rewrite /r /fi /gi. have ef1 := (expansion_restr1 eF cl0). have eg1 := (expansion_restr1 eG cl0). have il:= (Nsucc_i lN). apply: (expansion_prop11 (CS_nat lN) ef1 eg1). rewrite LgV// [X in _ <c X] LgV //. move => i li ik ri. have iN:= NS_lt_nat ik nN. have lsin: (csucc i) <=c n by apply /cleSltP. have ssin:= (proj33 lsin). have issi:= (cleS iN). have ssi:= (proj33 issi). have isi:= (Nsucc_i iN). move:(expansion_restr1 eF lsin). move:(expansion_restr1 eG lsin). set f1 := (restr F (csucc i)). set g1 := (restr G (csucc i)). move=> ef1 eg1; move: ri. rewrite /r /fi /gi (expansion_prop7 ef1 (proj32 li)). rewrite (expansion_prop7 eg1 (proj32 li)). set f2 := (restr f1 i). set g2 := (restr g1 i). have si: sub (csucc i) (domain F) by rewrite df. have sj: sub (csucc i) (domain G) by rewrite dg. have ->: (restr F i = f2) by rewrite /f2 /f1 double_restr. have ->: (restr G i = g2) by rewrite /g2 /g1 double_restr. have ->: (Vg f1 i = Vg g1 i). rewrite /f1 /g1 LgV // [RHS] LgV //; apply: pFG=>//. apply/cleSlt0P; fprops. have ef2 := (expansion_restr1 eg1 issi). have eg2 := (expansion_restr1 ef1 issi). apply: csum_Mlteq. apply: NS_prod; fprops; apply: (expansion_prop1 ef1); fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)