proposition: Lemma pair_asym x y : pair_leq x y -> pair_leq y x -> x = y.
proof: Proof. move: x y=>[x1 x2][y1 y2][/= H1 H2][/= H3 H4]. by congr (_, _); apply: poset_asym. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)