proposition: Lemma nsv_cantor_ok x y: ordinalp x -> ordinalp y -> S x y = x +#o y.
proof: Proof. move => ox oy. have Hu u v: u = \0c -> ordinalp v -> S u v = u +#o v. by move => -> ou; rewrite (nsv_0n ou) natural_sumC natural_sum0. have Hv u v: v = \0c -> ordinalp u -> S u v = u +#o v. by move => -> ou; rewrite (nsv_n0 ou) natural_sum0. move: (omax_p1 (OS_degree ox) (OS_degree oy)). set n := omax(odegree x) (odegree y); move => [h1 h2]. move: (proj32 h1) => on. move: n on ox oy h1 h2 => n0 on0. pose hyp n := forall x y, ordinalp x -> ordinalp y -> odegree x <=o n -> odegree y <=o n -> S x y = x +#o y. move: x y; suff: hyp n0 by apply. case: (least_ordinal6 hyp on0) => //. set n := least_ordinal _ _; move => [on mleast] [] x y ox oy ldx ldy. case: (ozero_dichot ox) => xz; first by apply: Hu. case: (ozero_dichot oy) => yz; first by apply: Hv. move: (nsv_aux xz ldx) => [a [rx [la lrx ->]]]. move: (nsv_aux yz ldy) => [b [ry [lb lry ->]]]. rewrite (nsv_cantor_p2 on la lb lrx lry). rewrite (nsv_cantor_p2_ww on la lb lrx lry). move: (proj31_1 lrx) (proj31_1 lry) => orx ory. apply: f_equal. case: (ozero_dichot orx) => xrz; first by apply: Hu. case: (ozero_dichot ory) => yrz; first by apply: Hv. move: (the_cnf_p6 on xrz lrx) (the_cnf_p6 on yrz lry) => d1 d2. move: (omax_p1 (proj31_1 d1) (proj31_1 d2)) => [qa qb]. have /(oltP on): omax (odegree rx) (odegree ry) <o n. by rewrite/omax /Gmax; Ytac h. by move/mleast; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)