proposition: Lemma nsv_cantor_p3 p x y : ordinalp p -> x <o oopow p -> y <o oopow p -> S x y <o oopow p.
proof: Proof. move => op. by apply: (nsv_cantor_p1 op) => q /proj31_1 oq; apply:nsv_cantor_p2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)