proposition: Lemma ordinalsrP (r:relation) x: worder_rc r -> r x x -> ordinals r (ordinalr r x) = x.
proof: Proof. move => pa pb. set a := (ordinalr r x). have: (exists2 x, r x x & a = ordinalr r x) by exists x. move /(ordinalsP pa); set q := ordinals r a; move => [rqq qv]. ex_middle bad. case: (worderr_total (proj1 pa) rqq pb) => h. by move: (ordinalr_Mlt pa h bad) => [_]; rewrite qv. by move: (ordinalr_Mlt pa h (nesym bad))=> [_]; rewrite qv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)