proposition: Lemma CNFq_p0 e c n i: CNFq_ax e c n -> i <c n -> ordinalp (cantor_mon e c i).
proof: Proof. move => [pa pb pc pd] lin. apply:OS_prod2; first by apply:(OS_pow (proj32 pa) (pb _ lin)). exact:(proj31_1 (pc _ lin)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)