proposition: Lemma omax_p3 x y (c:= cardinal (omax (omax x y) omega0)): ordinalp x -> ordinalp y -> [/\ infinite_c c, inc x (cnext c) & inc y (cnext c)].
proof: Proof. move => ox oy. move:(omax_p2 (OS_omax ox oy)); rewrite -/c; move => [ca cb]. move: (omax_p1 ox oy) => [ta tb]. have aux: forall t, t <=o omax x y -> inc t (cnext c). move: (proj1 (CS_cnext (proj1 ca))) => oc. have od: (omax x y) <o (cnext c) by apply /(oltP oc). by move => t tc; apply /(oltP oc); apply: (ole_ltT tc od). by split => //; apply: aux. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)