proposition: Lemma the_expansion_zero: the_expansion \0c = emptyset.
proof: Proof. move: (the_expansion_pr NS0) => sa. have hh: exp_boundary emptyset \0c by left. suff: expansion_normal_of emptyset b \0c \0c. move => sb; exact (proj1 (expansion_unique1 sa sb)). have H: expansion_value emptyset b = \0c. by rewrite /expansion_value domain_set0; apply: csum_trivial; aw. split; fprops;split => //; split;fprops; split; aw => //. + apply: fgraph_set0. + by move => i /in_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)