proposition: Lemma expe_0 : Nbexp \0c = \1c.
proof: Proof. rewrite /Nbexp. suff: (expansions_ext_of \0c) = singleton emptyset. by move => ->; rewrite cardinal_set1. apply:set1_pr. move: NS0 NS3 => ra rb. have ha:fgraph emptyset by apply: fgraph_set0. have hb:domain emptyset = emptyset by rewrite domain_set0. have hc:range emptyset = emptyset by rewrite range_set0. have hd:expansion_value emptyset \2c = \0c. by rewrite /expansion_value /csumb; aw; rewrite csum_trivial//;aw. have lt1: \1c <c \3c. rewrite - succ_zero; apply/(cltSSP CS0 CS2); apply: clt_02. have he: cardinal (domain emptyset) = \0c by rewrite hb cardinal_set0. have hf: expansion_ext_of emptyset (cardinal (domain emptyset)) \0c. hnf; rewrite he;split => //; split => //; rewrite hb. by split => // u /in_set0. apply/ Zo_P; split; last by split => //; left. apply/sub_fgraphsP; exists emptyset; fprops; apply/gfunctions_P2. split => //; rewrite hc; fprops. move => z za; move:(expe_bounded2 NS0 za) => /cle0 /card_nonempty. by move /domain_set0_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)