proposition: Lemma sub_asym x y : sub_leq x y -> sub_leq y x -> x = y.
proof: Proof. move: x y=>[x Hx][y Hy]; rewrite /sub_leq /= => H1 H2. move: (poset_asym H1 H2) Hy=> <- Hy; congr exist. by apply: proof_irrelevance. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype) LemmaOverloading(rels prelude)