proposition: Lemma expansion_unique f g b k: expansion f b k -> expansion g b k -> expansion_value f b = expansion_value g b -> f = g.
proof: Proof. move=> ef eg sm. have kN: natp k by move: eg => [_ kN _ _ ]. move: k kN f g sm ef eg. apply: Nat_induction. rewrite /expansion. move=> f1 g1 sv [bN _ _ [fgf df _]] [_ _ _ [fgg dg _]]. by apply: fgraph_exten; [exact | exact | ue | rewrite df;move=> x /in_set0 ]. move=> n nN pn f g sv ef eg. have cn: cardinalp n by fprops. have p1:= (expansion_prop10 cn ef). have p2:= (expansion_prop10 cn eg). have er1:=(expansion_prop5 ef cn). have er2:= (expansion_prop5 eg cn). have egN :=(expansion_prop3 eg). have q1N:= (expansion_prop6 ef cn). have q2N:= (expansion_prop6 eg cn). have r1N:= (expansion_prop3 er1). have r2N:= (expansion_prop3 er2). rewrite sv in p1. have bN: natp b by move: ef => [bN _]. have cpN: natp (b ^c n) by fprops. have bnz: (b ^c n <> \0c). have [_ b0]: (\0c <c b) by move: ef => [_ _ /(cle_ltT cle_01) ]. by apply: cpow_nz => bz; case: b0. move: (cdivision_unique egN cpN q1N r1N q2N r2N bnz p1 p2)=> [pt r]. have aux: (restr f n = restr g n) by apply: pn =>//. move:ef eg=> [_ _ _ [fgf df _]] [_ _ _ [fgg dg _]]. apply: fgraph_exten; [ exact | exact | ue | move=> x xdf /=]. case: (equal_or_not x n); first by move => ->. move=> xn. have xc: (inc x n). by move:xdf; rewrite df (succ_of_nat nN); case/setU1_P. have <-: (Vg (restr f n) x = Vg f x) by rewrite LgV. have <-: (Vg (restr g n) x = Vg g x) by rewrite LgV. ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)