proposition: Lemma nat_lemma : forall a : nat, Some (Init.Nat.pred (Pos.to_nat (Pos.of_nat (S a)))) = Some a.
proof: Proof. intros; apply f_equal. rewrite Nat2Pos.id; auto. Qed.
imports: PArith List ChoiceFacts Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool) Classes RandomQC Generators Sets