proposition: Lemma fkind_or_p2 a b (x := J val_or (J a b)): formulap a -> formulap b -> (formulap x /\ formula_len x = csucc (cmax (formula_len a) (formula_len b))).
proof: Proof. move => fa fb. move:(formula_len_pr fa); set n := formula_len a;move => [nN pa pb]. move:(formula_len_pr fb); set m := formula_len b;move => [mN pc pd]. move: (cmax_p1 (CS_nat nN) (CS_nat mN)). set p := cmax n m; move => [max1 max2]. have pN: natp p by apply: Gmax_E. have pe: inc x (Vf formulas_rec (csucc p)). rewrite (formulas_rec_succ pN). apply/next_formulasP; constructor 3; rewrite /x; aw; split; fprops. exact:(flength_rec fa max1 pN). exact:(flength_rec fb max2 pN). have fx:=(formula_hi (NS_succ pN) pe). split => //. move: val_compare => [q0 q1 q2 q3 [q4 q5 q6 [q7 q8 q9]]]. move:(formula_len_pr fx); set q := formula_len x;move => [qN pa' pb']. case: (equal_or_not q \0c) => qnz. move: pa'; rewrite qnz formulas_rec0 => /(fkind_pa fx). rewrite /x; aw; case => h; [by case:q4 | by case: q1]. move:(cpred_pr qN qnz) => [sa sb]. move: pa'; rewrite sb (formulas_rec_succ sa) => /next_formulasP; case. + by move/(pb' _ sa); move: (cltS sa); rewrite - sb => su /(cltNge su). + by rewrite /x; aw;move => [_ ha _]; case:C0_ne_C1. + move => [px Px qa qb qc]. move: qb; rewrite /x; aw; move/(pb _ sa) => ha. move: qc; rewrite /x; aw; move/(pd _ sa) => hb. move: (cmax_p0 ha hb); rewrite -/p => hc. move /(cleSSP (CS_nat pN) (CS_nat sa)): hc; rewrite - sb. move: (pb' _ (NS_succ pN) pe); apply: cleA. + by rewrite /x; aw;move => [_ h _ _ _]; case: q8. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)