fact: Definition rangePos (p : positive) : list positive := map Pos.of_nat (rangeNat (Pos.to_nat p)).
imports: PArith List ChoiceFacts Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool) Classes RandomQC Generators Sets