proposition: Lemma ord_sup_pr6 E: ordinal_set E -> greatest (ole_on (E +s1 (\osup E))) (\osup E).
proof: Proof. move=> Ep; move: (OS_sup Ep) => os. have ee: ordinal_set (E +s1 (union E)). move => y; case/setU1_P;[apply: Ep | move=> ->; exact]. move: (wordering_ole_pr ee) => [p0 p1]. red; aw. rewrite p1;split; first by fprops. move => x xt; apply /graph_on_P1;split;fprops. move: xt; case /setU1_P; first by apply: ord_sup_ub =>//. by move => ->; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)