proposition: Lemma Qpairio_osr: order_on Qpairi_o Qpairis.
proof: Proof. move:(sub_osr Qpairis) => [pa pb]. move: (opp_osr pa) => [pc pd]. rewrite /Qpairi_o /order_on; split => //; ue. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)