proposition: Lemma wordering_ole_pr x: ordinal_set x -> worder_on (ole_on x) x.
proof: Proof. move => osx. by apply: wordering_pr; [apply: wordering_ole | move => a /osx ox; split]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)