proposition: Lemma pair_trans x y z : pair_leq x y -> pair_leq y z -> pair_leq x z.
proof: Proof. move: x y z=>[x1 x2][y1 y2][z1 z2][/= H1 H2][/= H3 H4]; split=>/=. - by apply: poset_trans H3. by apply: poset_trans H4. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)