intro v
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
⊢ ∀ (i_1 : Vector ℕ n),
    Part.map ((fun v x => x.isLeNat (v.get j)) i_1)
        (rfind fun n_1 =>
          Part.some
            (decide
              (0 <
                (((n_1 ::ᵥ i_1).head * (n_1 ::ᵥ i_1).get i.succ).isEqNat ((n_1 ::ᵥ i_1).get j.succ)).or
                  (((n_1 ::ᵥ i_1).get j.succ).isLtNat (n_1 ::ᵥ i_1).head)))) =
      (↑fun v => (v.get i).isDvdNat (v.get j)) i_1
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
⊢ Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head)))) =
    (↑fun v => (v.get i).isDvdNat (v.get j)) v