proposition: Lemma ordinal_pr1 E: ordinalp E <-> [/\ transitive_set E, worder (ordinal_oa E) & asymmetric_set E].
proof: Proof. split. move=> oE; split => //. - by apply: ordinal_transitive. - by apply: ordinal_worder. - move=> x y xE yE xy yx. have ox:= (Os_ordinal oE xE). have xx:=(ordinal_transitive ox yx xy). by case:(ordinal_irreflexive ox xx). move=> [tE woE aE] X XE tX nXE. have de: decent_set E by move=> u uE uu; case: (aE _ _ uE uE uu uu). have p0:forall b, inc b E -> inc b b \/ b = b by move=> b bE; right. have sg: (substrate (ordinal_oa E)) = E by rewrite /ordinal_oa graph_on_sr. have si: segmentp (ordinal_oa E) X. rewrite /segmentp /interval_uo /ordinal_oa sg; split => //. move=> x y xX /graph_on_P1 [yE _ h]. case: h; [ apply: (tX _ xX) | by move => -> ]. case: (well_ordered_segment woE si). by rewrite sg; move=> eXE. by rewrite sg; move=> [x xs ->]; rewrite ordinal_segment1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)