proposition: Lemma ordering_pair4 x: ordinal_pair x -> ord_pair_le x x.
proof: Proof. move => op; hnf; split => //; right; split => //; right; split => //. by move:op => [_ _ ok]; apply: oleR. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)