proposition: Lemma ord_cofinal_p2 A B: limit_ordinal B -> sub A B -> (ord_cofinal A B <-> \osup A = \osup B).
proof: Proof. move => pa pb; move: (pa) => [ob _ _]; split. by move => [_ pc]; apply: ord_sup_1cofinal => // x /(Os_ordinal ob). move => pc; split => // x xb. have ox:=(Os_ordinal ob xb). have osa:= (Os_sub (Os_ordinal ob) pb). ex_middle h. have pd: forall y, inc y A -> y <o x. move => y ya. case (oleT_el ox (osa _ ya)) => // pe; case h; ex_tac. have sb: \osup B <=o x by rewrite - pc; apply: ord_ub_sup => // i /pd []. move: xb sb. by rewrite -[union B](limit_nonsucc pa); move /(oltP ob) => ua /(oltNge ua). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)