proposition: Lemma the_expansion_digit a: a <> \0c -> a <c b -> the_expansion a = singleton (J \0c a).
proof: Proof. move => abz alb. have aN :=(NS_lt_nat alb bN). have n1:= NS1. move: (the_expansion_pr aN) => sa. move: (simple_fct2 \0c a); set f := singleton (J \0c a). move => [ra rb rc rd re]. have rf:Vg f \0c *c b ^c \0c = a by rewrite rd cpowx0 (cprod1r (CS_nat aN)). have rg: expansion_value f b = a. by rewrite /expansion_value rb csum_trivial3 rf (card_nat aN). suff: expansion_normal_of f b \1c a. move => sb; exact (proj1 (expansion_unique1 sa sb)). split; last by right; split; [ apply: card1_nz | by rewrite cpred1 rd]. split => //; split => //; rewrite rb; split => //. move => i /set1_P ->; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)