fact: Fixpoint pathToPosAux (p : SplitPath) (f : positive -> positive) : option positive := match p with | [Right] => Some (f xH) | Left :: Right :: p' => pathToPosAux p' (fun p => xI (f p)) | Left :: Left :: p' => pathToPosAux p' (fun p => xO (f p)) | _ => None end.
imports: PArith List ChoiceFacts Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool) Classes RandomQC Generators Sets