proposition: Lemma ord_sup_prop E: ordinal_set E -> exists! x, ordinalp x /\ (forall y, x <=o y <-> (ordinalp y /\ ordinal_ub E y)).
proof: Proof. move=> alo; set p := fun x: Set => _; apply /unique_existence;split. have ou:= (OS_sup alo). exists (\osup E); split => // y; split. move => h. have oy:= (proj32 h). split => //; move=> i iE; exact (oleT (ord_sup_ub alo iE) h). by move=> [oy aly]; apply:ord_ub_sup. have p1: forall x, p x -> ordinal_ub E x. move=> t [ox Ex]. by move: (oleR ox); rewrite (Ex t); move => [_]. have p2: forall x y, p x -> ordinalp y -> (ordinal_ub E y) -> x <=o y. move=> x1 y1 [ox opf] oy h; rewrite opf; split => //. move=> x y fx fy. exact: (oleA (p2 _ _ fx (proj1 fy) (p1 _ fy)) (p2 _ _ fy (proj1 fx) (p1 _ fx))). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)