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