proposition: Lemma CNFq_exten e1 c1 e2 c2 n: same_below e1 e2 n -> same_below c1 c2 n -> CNFq_ax e1 c1 n -> natp n -> (CNFq_ax e2 c2 n /\ CNFbv e1 c1 n = CNFbv e2 c2 n).
proof: Proof. move => h1 h2 ax nN; split; first by apply: (CNFq_ax_exten h1 h2 ax). apply: (osumf_exten nN) => i lin. by rewrite /cantor_mon (h1 _ lin) (h2 _ lin). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)