proposition: Lemma CNFq_m_ax e1 c1 e2 c2 k m: natp k -> natp m -> CNFq_ax e1 c1 k -> CNFq_ax e2 c2 m -> (m = \0c \/ e1 (cpred k) <o e2 \0o) -> (CNFq_ax (cnf_m e1 e2 k) (cnf_m c1 c2 k) (k +c m)).
proof: Proof. move => kN mN [p1 p2 p3 p4] [q1 q2 q3 q4] hs. 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: (cleT_el (CS_nat kN) (CS_nat 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. rewrite/cnf_m; split. + done. + move => i /aux []; first by move => ik;by Ytac0; apply: p2. by move => [nik likm]; Ytac0; apply: q2. + move => i /aux []; first by move => ik;by Ytac0; apply: p3. by move => [nik likm]; Ytac0; apply: q3. + move => i iN lis; case:(aux _ lis). move => lt1; move: (cle_ltT (cleS iN) lt1) => li1. by Ytac0; Ytac0; apply:p4. move => [pa pb]; Ytac0. case: hs => hs; first by move: pb; rewrite hs => /clt0. have ci:= (CS_nat iN). have ck:= (CS_nat kN). case: (cleT_ell ck (CS_succ i)) => //. move:(cltS iN) => lt1 sa; rewrite sa cdiff_nn; Ytac0. have -> //: i = cpred k by rewrite sa cpred_pr1. move => /(cltSleP iN) ki. case: (aux _ (cle_ltT (cleS iN) lis)); first by move => /(cleNgt ki). move => [pc pd]; Ytac0. have sa: csucc i -c k = csucc (i-c k). move: (cdiff_pr4 kN iN NS0 NS1 ki cle_01). rewrite (csucc_pr4 ci) (csum0r ck) (cdiff_n0 NS1) csucc_pr4 //. exact: (proj31_1 pd). rewrite sa; apply: (q4 _ (NS_diff k iN)); ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)