proposition: Lemma expansion_prop14 f g b kf kg: expansion f b kf -> expansion g b kg -> (expansion_value f b) <c (expansion_value g b) -> (exists l, [/\ kf <=c l, l <c kg & Vg g l <> \0c]) \/ ( exists 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) & (Vg f l) <c (Vg g l)]]).
proof: Proof. move=> ef eg lt. have kfN:natp kf by move: ef => [_ h _]. have kgN:natp kg by move: eg => [_ h _]. have [n [nf ng nfg]]: exists n, [/\ n <=c kf, n <=c kg & (n = kf \/ n = kg)]. case: (NleT_ee kfN kgN)=> aux; [exists kf | exists kg];split;fprops. have nN: natp n by case: nfg => ->. case: (p_or_not_p (forall i, n <=c i -> i <c kg -> Vg g i = \0c)); last first. move=> h. have [i [ni ik Vz]]: (exists i, [/\ n <=c i, i <c kg & Vg g i <> \0c]). ex_middle h'; case: h => i i1 i2; ex_middle h''; case h'; exists i => //. left; exists i; split => //. case: nfg; [by move=> <- | move=> nk; case:(cltNge ik); ue ]. move=> pB; right. case: (p_or_not_p (forall i, n <=c i -> i <c kf -> Vg f i = \0c)); last first. move=> h. have [i [ni ik Vz]]: (exists i, [/\ n <=c i, i <c kf & Vg f i <> \0c]). ex_middle h'; case: h => i i1 i2; ex_middle h''; case h'; exists i => //. have fi: kg <=c i. case: nfg; [ move => nk; case: (cltNge ik); ue | by move=> <-]. by move: (expansion_prop13 fi ik eg ef Vz) =>[ /(cltNge lt)]. move=> pA. move: (ef) (eg) => [bN bK b2 [fgf df vf]][_ _ _ [fgg dg vg]]. have pC: exists2 l, l <c n& (Vg f l) <> (Vg g l). have hf:= (expansion_restr2 ef nf pA). have hg:= (expansion_restr2 eg ng pB). ex_middle bad. have eq: (restr f n = restr g n). have s1: sub n (domain g) by rewrite dg; apply: (proj33 ng). have s2: sub n (domain f) by rewrite df; apply: (proj33 nf). have drf: (domain (restr f n) = n) by aw. have drg: (domain (restr g n) = n) by aw. apply: fgraph_exten; fprops; first ue. rewrite drf => x xdf; rewrite !LgV //. ex_middle nx; case: bad; exists x => //. by move: xdf => /(NltP nN). move: lt;rewrite -hf -hg eq; move => [_ ne]; case: ne; reflexivity. have [l [lp ln Vl]]: exists l, [/\ (forall i, l <c i -> i <c n -> Vg f i = Vg g i), l <c n & (Vg f l) <> (Vg g l)]. set z:= Zo Nat (fun l => l <c n /\ Vg f l <> Vg g l). have nz: nonempty z. move: pC => [l lp]; exists l; apply: Zo_i => //; apply: (NS_lt_nat lp nN). have pa: (forall a, inc a z -> cardinalp a) by move=> a /Zo_P [aN _ ]; fprops. have [wor sr]:= (wordering_cle_pr pa). have tor := (worder_total wor). have zc: sub z (Nint n) by move=> t /Zo_P [_ [p1 _]]; apply /NintP. have fsz: finite_set z by apply: (sub_finite_set zc); apply: finite_Nint. have sw: sub z (substrate (graph_on cardinal_le z)) by rewrite sr; fprops. have or := proj1 wor. move: (finite_subset_torder_greatest tor fsz nz sw)=> [l []]. rewrite iorder_sr //; move=> lz lp; exists l. move: (lz); move => /Zo_P [lN [ln Vl]]; split => //. move=> i li lin; ex_middle h. have iN:= NS_lt_nat lin nN. have iz: inc i z by apply: Zo_i => //. by move: (iorder_gle1 (lp _ iz)) => /graph_on_P1 [_ _ /(cltNge li)]. exists l; exists n; split => //. have p1: cardinalp (Vg f l). have ldf: (inc l (domain f)). rewrite df; apply /NltP => //; apply:clt_leT ln nf. exact: (proj31_1 (vf _ ldf)). have p2: cardinalp (Vg g l). have ldf: (inc l (domain g)). rewrite dg; apply /NltP => //; apply:clt_leT ln ng. exact: (proj31_1 (vg _ ldf)). case: (cleT_el p2 p1) => // h. have p3: (Vg g l) <c (Vg f l) by split => //; apply: nesym. have lp' : forall i, l <c i -> i <c n -> Vg g i = Vg f i. by move=> i i1 i2; symmetry;move: (lp _ i1 i2). case: (cltNge lt (proj1(expansion_prop12 ng nf ln pB pA lp' eg ef p3))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)