proposition: Lemma ordinal_segment1 E x: trans_dec_set E -> inc x E -> segment (ordinal_oa E) x = x.
proof: Proof. move => [tE dE] xE. suff: segment (ordinal_oa E) x = x \cap E. by move => ->; apply/setI2id_Pl; apply: tE. rewrite /segment /ordinal_oa /interval_uo graph_on_sr; last by fprops. set_extens y. by move/Zo_hi => [ /graph_on_P1 [pa pb pc] pd]; apply: setI2_i => //;case: pc. move /setI2_P=> [yx yE]; apply:(Zo_i yE);split. by apply/graph_on_P1; split => //; left. move=> xy; rewrite xy in yx; case: (dE _ xE yx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)