proposition: Lemma ordinalrsP (p: property) (r := fun x y => [/\ p x, p y & x <=o y]) x (y := ordinalr r x): ordinal_prop p -> p x -> (ordinalp y) /\ ordinals r y = x.
proof: Proof. move => op px; move:(op _ px) => ox. move: (worder_rc_op p) => pa. have rxx: r x x by split => //; apply:oleR. move:(ordinalsrP pa rxx) => h; split => //; by apply: OS_ordinalr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)