fact: Definition posS (n : nat) : pos := @pos_of n.+1 isT.
imports: HB(structures) ZArith mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp) mathcomp(path choice fintype tuple finset ssralg ssrnum bigop ssrint) CoqEAL(hrel param refinements)