proposition: Lemma expansion_unique1 a f k f' k': expansion_normal_of f b k a -> expansion_normal_of f' b k' a -> f = f' /\ k = k'.
proof: Proof. move => [[ha hb] hc] [[ha' hb'] hc']. have kN: natp k by case: ha. have kN': natp k' by case: ha'. wlog: k k' f f' ha hb hc ha' hb' hc' kN kN'/ k <c k'. case: (NleT_ell kN' kN) => h H; last by apply:H. rewrite h in ha'; rewrite - hb' in hb. split => //; exact: (expansion_unique ha ha' hb). by case:(H _ _ _ _ ha' hb' hc' ha hb hc kN' kN h) => [-> ->]. move => h. case: hc'; first by move => e1; rewrite e1 in h; case: (clt0 h). move => [e1 e2]. move: (cpred_pr kN' e1) => [sa sb]. have k1: k <=c (cpred k') by apply /(cltSleP sa); rewrite - sb. have k2: (cpred k') <c k' by rewrite {2} sb; apply: cltS. by move: (proj2 (expansion_prop13 k1 k2 ha ha' e2)); rewrite hb hb'. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)