proposition: Lemma poset_asym (x y : T) : x <== y -> y <== x -> x = y.
proof: Proof. by case: T x y=>S [[l b B R A Tr]] *; apply: (A). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)