proposition: Lemma posLtInRange : forall max pos, Pos.le pos max -> In pos (rangePos max).
proof: Proof. intros. apply in_map_iff. exists (Pos.to_nat pos). split. - apply Pos2Nat.id. - apply ltInRange. + apply Pos2Nat.inj_le; auto. + pose proof (Pos2Nat.is_succ pos) as Contra; inversion_clear Contra; congruence. Qed.
imports: PArith List ChoiceFacts Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool) Classes RandomQC Generators Sets