proposition: Lemma CNFb_s_ax e c n k m: CNFb_ax e c m -> (n +c k) <=c m -> natp k -> natp n -> CNFb_ax (cnf_s e k) (cnf_s c k) n.
proof: Proof. move => [p1 p2] mn kN nN; split; first by apply: (CNFq_s_ax p1 mn kN nN). by move => i lin; apply: p2; move:(clt_leT (csum_Mlteq kN lin) mn). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)