proposition: Lemma ord_sup_1cofinal x y: ord_cofinal x y -> ordinal_set y -> \osup x = \osup y.
proof: Proof. move=> [h1 h2] h3; apply: ord_sup_2cofinal; split => // a ay;exists a;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)