proposition: Lemma von_neumann_ordinal E: ordinalp E <-> (worder (ordinal_o E) /\ (forall x, inc x E -> segment (ordinal_o E) x = x)).
proof: Proof. split. move => oE; split; first by apply: (ordinal_o_wor oE). by move => x xE;apply:ordinal_segment. move => [sa sb]. have Ha y x: inc x E -> inc y x -> ssub y x. by move => xE; rewrite -{1} (sb _ xE); move/segmentP => [/ordo_leP []]. have tE: transitive_set E. by move => x xE y; rewrite - (sb _ xE); move/segmentP => [/ordo_leP []]. have aE: asymmetric_set E. move => y z yE zE /(Ha _ _ zE) [pa pb] /(Ha _ _ yE) [pc _]. by case: pb; apply:extensionality. suff: (ordinal_o E) = (ordinal_oa E). by move => h; rewrite h in sa;apply/ordinal_pr1. have g1: sgraph (ordinal_o E) by move: (ordinal_o_or E) => []. have g2: sgraph (ordinal_oa E) by move => t /Zo_S /setX_P []. apply:sgraph_exten => // u v. rewrite /ordinal_oa. split => /graph_on_P1 [uE vE h]; apply /graph_on_P1; split => //. case: (equal_or_not u v) => euv; [by right | left]. by rewrite -(sb _ vE); apply/segmentP; split => //; apply/ordo_leP. case: h; [ move => ub; exact (proj1(Ha _ _ vE ub)) | by move ->]. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)