fact: Definition chain_axiom (s : Pred T) := (exists d, d \In s) /\ (forall x y, x \In s -> y \In s -> x <== y \/ y <== x).
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)