proposition: Lemma CNFb_m_ax e1 c1 e2 c2 k m: natp k -> natp m -> CNFb_ax e1 c1 k -> CNFb_ax e2 c2 m -> (m = \0c \/ e1 (cpred k) <o e2 \0o) -> (CNFb_ax (cnf_m e1 e2 k) (cnf_m c1 c2 k) (k +c m)).
proof: Proof. move => kN mN [p1 p2] [p3 p4] h1. split; first by apply:CNFq_m_ax. have aux: forall i, i <c k +c m -> i <c k \/ (~ (i <c k) /\ (i -c k) <c m). move => i lik. move:(NS_lt_nat lik (NS_sum kN mN))=> iN. case: (NleT_el kN iN); last by left. move => ki; move: (cdiff_pr ki) => s1. right; split; first by move=> /(cleNgt ki). apply: (csum_lt2l kN (NS_diff k iN) mN); ue. move => i /aux []; first by move => ik;by rewrite /cnf_m; Ytac0; apply: p2. by move => [nik likm]; rewrite /cnf_m; Ytac0; apply: p4. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)