fact: Definition ord_pair_le x y:= [/\ ordinal_pair x, ordinal_pair y & (ord_pair_max x <o ord_pair_max y \/ (ord_pair_max x = ord_pair_max y /\ ((P x) <o (P y) \/ (P x = P y /\ Q x <=o Q y))))].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)