proposition: Lemma ordinalsP (r:relation) a: worder_rc r -> (exists2 x, r x x & a = ordinalr r x) -> (r (ordinals r a) (ordinals r a) /\ ordinalr r (ordinals r a) = a).
proof: Proof. move => pa [x rxx av]. pose p x := (r x x /\ a = ordinalr r x). rewrite /ordinals -/p. have exp : exists x, p x by exists x. by move: (choose_pr exp); set q := (choose p); move => [rqq ->]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)