∀ (s : String) (begPos : String.Pos.Raw) (p : Char → Bool) (i : String.Pos.Raw),
  Substring.Raw.takeRightWhileAux s begPos p i =
    if h : begPos < i then
      have this := ⋯;
      have i' := String.Pos.Raw.prev s i;
      have c := String.Pos.Raw.get s i';
      if (!p c) = true then i else Substring.Raw.takeRightWhileAux s begPos p i'
    else i