proposition: Lemma CNFq_s_ax e c n k m: CNFq_ax e c m -> (n +c k) <=c m -> natp k -> natp n -> CNFq_ax (cnf_s e k) (cnf_s c k) n.
proof: Proof. move => [p1 p2 p3 p4] mn kN nN. have aux: forall i, i <c n -> i +c k <c m. by move => i lin; move:(clt_leT(csum_Mlteq kN lin) mn). split. + done. + by move => i /aux /p2. + by move => i /aux /p3. + move => i iN /aux; rewrite /cnf_s (csum_Sn _ iN); apply: p4; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)