proposition: Lemma fkind_not_p2 a (x := J val_not a): formulap a -> (formulap x /\ formula_len x = csucc (formula_len a)).
proof: Proof. move: val_compare => [q0 q1 q2 q3 [q4 q5 q6 [q7 q8 q9]]]. move => fa. move:(formula_len_pr fa); set n := formula_len a;move => [nN pa pb]. have pc: inc x (Vf formulas_rec (csucc n)). rewrite (formulas_rec_succ nN). apply/next_formulasP; constructor 2;rewrite /x; aw;split; fprops. have fx:=(formula_hi (NS_succ nN) pc). split => //. move:(formula_len_pr fx); set m := formula_len x;move => [mN pa' pb']. move:(pb' _ (NS_succ nN) pc) => le1. case: (equal_or_not m \0c) => mnz. move: pa'; rewrite mnz formulas_rec0 => /(fkind_pa fx). rewrite /x; aw; case => h; [by case:q5 | by case: q2]. move:(cpred_pr mN mnz) => [vc vb]. move: pa'; rewrite vb (formulas_rec_succ vc) => /next_formulasP; case. + by move/(pb' _ vc); move: (cltS vc); rewrite - vb=> su /(cltNge su). + move => [_ _]; rewrite /x; aw; move/(pb _ vc) => he. move /(cleSSP (CS_nat nN) (CS_nat vc)): he; rewrite - vb => le. by apply: cleA. + by move => [_ hh _ _ _]; case: q7; rewrite - hh; rewrite /x; aw. + by move => [_ hh _ _ _]; case: q9; rewrite - hh; rewrite /x; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)