proposition: Lemma ord_sup_2cofinal x y: mutually_cofinal x y -> \osup x = \osup y.
proof: Proof. move=> [p3 p4]. have osx: ordinal_set x by move => a ax; move: (p3 _ ax) => [b _ []]. have osy: ordinal_set y by move => a ay; move: (p4 _ ay) => [b _ []]. apply: oleA. apply: ord_ub_sup => //; first by apply: OS_sup. move=> i ix; move: (p3 _ ix) => [j jy lij]. apply: (oleT lij);apply ord_sup_ub => //. apply: ord_ub_sup => //; first by apply: OS_sup. move=> i ix; move: (p4 _ ix) => [j jy lij]. apply: (oleT lij);apply: ord_sup_ub => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)