proposition: Lemma flength_nz x (n := formula_len x) (F := (Vf formulas_rec (cpred n))): formulap x -> n <> \0c -> [/\ natp (cpred n), inc x (next_formulas F) & ~ inc x F].
proof: Proof. move => fp nz. move:(formula_len_pr fp) => []; rewrite -/n => nN qa qb. move:(cpred_pr nN nz) => [mN mv]. move: qa; rewrite {1} mv (formulas_rec_succ mN) -/F => qc; split => // xF. by move:(qb _ mN xF)(cltS mN); rewrite - mv => l1 /(cleNgt l1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)