proposition: Lemma fkind3_p1 x (a := Q x): formulap x -> P x = val_not -> [/\ x = J val_not a, formulap a & formula_len a <c formula_len x].
proof: Proof. move => fp kx1. move: val_compare => [q0 q1 q2 q3 [q4 q5 q6 [q7 q8 q9]]]. case (equal_or_not (formula_len x) \0c) => ha. move /(flength0P fp): ha => /atomic_formulaP [_ _ _ _]. rewrite kx1; case => h; [by case: q5 | by case: q2]. case:(flength_nz fp ha); set F:= Vf _ _ => pa pb pc. case/next_formulasP: pb. + done. + move => [prx _ aF]. rewrite {1} /a - kx1 prx. move:(NS_formula_len fp) => nN. move: (cpred_pr nN ha) => [sa ->]. have fa:= (formula_hi sa aF); split => //; apply/(cltSleP sa). exact:(proj33 (formula_len_pr fa) _ sa aF). + by move => [_ h _ _ _];case:q7; rewrite - h. + by move => [_ h _ _ _];case:q9; rewrite - h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)