proposition: Lemma sub_trans x y z : sub_leq x y -> sub_leq y z -> sub_leq x z.
proof: Proof. move: x y z=>[x Hx][y Hy][z Hz]; rewrite /sub_leq /=. by apply: poset_trans. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)