proposition: Lemma Qpairio_gleP x y: gle Qpairi_o x y <-> [/\ inc x Qpairis, inc y Qpairis & sub y x].
proof: Proof. apply: (iff_trans (opp_gleP _ _ _)). split; first by move /sub_gleP => [p1 p2 p3]. by move => [pa pb pc]; apply /sub_gleP. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)