proposition: Lemma nat_chain_axiom : chain_axiom (@PredT nat).
proof: Proof. split=>[|x y _ _]; first by exists 0. rewrite /Poset.leq /= [y <= x]leq_eqVlt. by case: leqP; [left | rewrite orbT; right]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)