proposition: Lemma CNFq_A e c n m: natp n -> natp m -> CNFq_ax e c (n +c m) -> [/\ CNFq_ax e c n, CNFq_ax (cnf_s e n) (cnf_s c n) m & CNFbv e c (n +c m) = CNFbv (cnf_s e n) (cnf_s c n) m +o CNFbv e c n].
proof: Proof. move => nN mN ax. have pa: ord_below (cantor_mon e c) (n +c m). by move => i; apply:CNFq_p0. rewrite /CNFbv (osum_fA nN mN pa). have lt1: n <=c n +c m by apply:Nsum_M0le. have hb: CNFq_ax e c n by apply:(CNFq_r_ax ax lt1). have hc //: CNFq_ax (cnf_s e n) (cnf_s c n) m. have hh:m +c n <=c n +c m by rewrite csumC; exact: (cleR (proj32 lt1)). exact:(CNFq_s_ax ax hh nN mN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)