proposition: Lemma size_p f (s := size f): inc f dexpansions -> [/\ natp s, forall m, natp m -> s <=c m -> Vf f m = \0c & s = \0c \/ [/\ natp (cpred s), csucc (cpred s) = s & Vf f (cpred s) <> \0c]].
proof: Proof. move=> /Zo_P [ff [q qN qp]]; rewrite /s /size. set E:= Zo _ _. have ha: sub E Nat by apply: Zo_S. have hb: nonempty E by exists q; apply: Zo_i. move:(@inf_Nat E ha hb) =>[/Zo_P[qa qb] qc]; split => //. case:(equal_or_not (intersection E) \0c) => ee; [by left | right]. move:(cpred_pr qa ee); set n := cpred _; move => [pN pv]. split => // fnz. case:(cltNge (cpred_lt qa ee)). have/ qc //: inc n E. apply:(Zo_i pN) => m mN; case/cle_eqVlt; first by move => <-. by move/(cleSltP pN); rewrite - pv; apply: qb. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)