have := rfindPos₁ i (f := F) <| (Arith₁.and 0 1).comp₂ _
    ((Arith₁.le 0 1).comp₂ _ (hf.comp₁ _ (proj 0)) (proj 1))
    ((Arith₁.lt 0 1).comp₂ _ (proj 1) (hf.comp₁ _ $ (Arith₁.succ 0).comp₁ _ $ proj 0))
n : ℕ
i : Fin n
f : ℕ → ℕ
hf : Arith₁ fun v => f (v.get 0)
F : ℕ → ℕ → ℕ := fun x y => ((f x).isLeNat y).and (y.isLtNat (f (x + 1)))
⊢ ArithPart₁ fun v => Nat.rfind fun x => Part.some (decide (f x ≤ v.get i ∧ v.get i < f (x + 1)))
n : ℕ
i : Fin n
f : ℕ → ℕ
hf : Arith₁ fun v => f (v.get 0)
F : ℕ → ℕ → ℕ := fun x y => ((f x).isLeNat y).and (y.isLtNat (f (x + 1)))
this : ArithPart₁ fun v => Nat.rfind fun n_1 => Part.some (decide (0 < F n_1 (v.get i)))
⊢ ArithPart₁ fun v => Nat.rfind fun x => Part.some (decide (f x ≤ v.get i ∧ v.get i < f (x + 1)))