ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<GOAL>∀ {α : Type u_1} {a : α} {acc : List α} (n : Nat), List.replicateTR.loop a n acc = List.replicate n a ++ acc
<VAR>α : Type u_3<VAR>β : Type u_2<VAR>γ : Type u_1<VAR>f : α → β → γ<VAR>as : List α<VAR>bs : List β<VAR>acc : Array γ<GOAL>List.zipWithTR.go f as bs acc = acc.data ++ List.zipWith f as bs
<VAR>α : Type u_1<VAR>l : List α<VAR>n : Nat<GOAL>let f := fun a x => match x with | (n, acc) => (n - 1, (n - 1, a) :: acc);
List.foldr f (n + l.length, []) l = (n, List.enumFrom n l)
<VAR>α : Type u_1<VAR>sep : List α<VAR>acc : Array α<VAR>x : List α<VAR>xs : List (List α)<GOAL>List.intercalateTR.go (List.toArray sep) x xs acc = acc.data ++ (List.intersperse sep (x :: xs)).join
<VAR>a b : UInt8<GOAL>a % b = { val := a.val % b.val }
<VAR>a b : UInt8<GOAL>¬a ≤ b ↔ b < a
<VAR>a b c : UInt8<GOAL>a < b → b < c → a < c
<VAR>m : Nat<VAR>u : UInt8<GOAL>m > 0 → (u % m).toNat < m
<VAR>a b : UInt8<GOAL>a * b = { val := a.val * b.val }
<VAR>a b : UInt8<GOAL>a - b = { val := a.val - b.val }
<VAR>a : Nat<GOAL>a < UInt8.size → ↑(UInt8.ofNat a).val = a
<VAR>a : UInt8<VAR>b : Nat<GOAL>(a.modn b).toNat = a.toNat % b
<VAR>a b c : UInt8<GOAL>a ≤ b → b ≤ c → a ≤ c
<VAR>a b : UInt8<VAR>h : a < b<GOAL>¬b < a
<VAR>a b : UInt8<GOAL>¬a < b ↔ b ≤ a
<VAR>a b : UInt8<VAR>h : a < b<GOAL>a ≠ b
<VAR>a b : UInt8<VAR>h : a = b<GOAL>a.val = b.val
<VAR>a b : UInt8<VAR>h : a.val = b.val<GOAL>a = b
<VAR>a b : UInt8<GOAL>a + b = { val := a.val + b.val }
<VAR>a : UInt8<GOAL>{ val := a.val } = a
<VAR>a b : UInt8<GOAL>a < b ↔ a.val < b.val
<VAR>a b : UInt8<GOAL>(a / b).toNat = a.toNat / b.toNat
<VAR>a b : UInt8<VAR>h : a.val ≠ b.val<GOAL>a ≠ b
<VAR>a b : UInt8<VAR>h : 0 < b<GOAL>a % b < b
<VAR>a b : UInt8<GOAL>(a % b).toNat = a.toNat % b.toNat
<VAR>a b : UInt8<GOAL>a ≤ b ↔ a.val ≤ b.val
<VAR>a b : UInt8<GOAL>a.toNat = b.toNat → a = b
<VAR>a b : UInt8<GOAL>a ≤ b ∨ b ≤ a
<VAR>a b : UInt16<GOAL>a - b = { val := a.val - b.val }
<VAR>a b c : UInt16<GOAL>a ≤ b → b ≤ c → a ≤ c
<VAR>a : UInt16<GOAL>{ val := a.val } = a
<VAR>a b : UInt16<GOAL>(a % b).toNat = a.toNat % b.toNat
<VAR>a b : UInt16<GOAL>a % b = { val := a.val % b.val }
<VAR>a : UInt16<VAR>b : Nat<GOAL>(a.modn b).toNat = a.toNat % b
<VAR>a b c : UInt16<GOAL>a < b → b < c → a < c
<VAR>a b : UInt16<GOAL>a * b = { val := a.val * b.val }
<VAR>a b : UInt16<GOAL>¬a < b ↔ b ≤ a
<VAR>a b : UInt16<GOAL>a ≤ b ↔ a.val ≤ b.val
<VAR>a b : UInt16<GOAL>¬a ≤ b ↔ b < a
<VAR>a b : UInt16<GOAL>a < b ↔ a.val < b.val
<VAR>a b : UInt16<GOAL>a.toNat = b.toNat → a = b
<VAR>a b : UInt16<GOAL>(a / b).toNat = a.toNat / b.toNat
<VAR>a : Nat<GOAL>a < UInt16.size → ↑(UInt16.ofNat a).val = a
<VAR>a b : UInt16<VAR>h : 0 < b<GOAL>a % b < b
<VAR>a b : UInt16<GOAL>a ≤ b ∨ b ≤ a
<VAR>a b : UInt16<VAR>h : a < b<GOAL>a ≠ b
<VAR>a b : UInt16<VAR>h : a < b<GOAL>¬b < a
<VAR>a b : UInt16<GOAL>a + b = { val := a.val + b.val }
<VAR>m : Nat<VAR>u : UInt16<GOAL>m > 0 → (u % m).toNat < m
<VAR>a b : UInt16<VAR>h : a.val ≠ b.val<GOAL>a ≠ b
<VAR>a b : UInt16<VAR>h : a.val = b.val<GOAL>a = b
<VAR>a b : UInt16<VAR>h : a = b<GOAL>a.val = b.val
<VAR>a : UInt32<GOAL>{ val := a.val } = a
<VAR>a b : UInt32<VAR>h : a < b<GOAL>a ≠ b
<VAR>a b : UInt32<GOAL>a + b = { val := a.val + b.val }
<VAR>a b : UInt32<VAR>h : a < b<GOAL>¬b < a
<VAR>a b : UInt32<GOAL>a < b ↔ a.val < b.val
<VAR>a : UInt32<VAR>b : Nat<GOAL>(a.modn b).toNat = a.toNat % b
<VAR>a b c : UInt32<GOAL>a ≤ b → b ≤ c → a ≤ c
<VAR>a b : UInt32<GOAL>¬a ≤ b ↔ b < a
<VAR>a b c : UInt32<GOAL>a < b → b < c → a < c
<VAR>a b : UInt32<GOAL>(a % b).toNat = a.toNat % b.toNat
<VAR>m : Nat<VAR>u : UInt32<GOAL>m > 0 → (u % m).toNat < m
<VAR>a b : UInt32<GOAL>(a / b).toNat = a.toNat / b.toNat
<VAR>a b : UInt32<VAR>h : 0 < b<GOAL>a % b < b
<VAR>a b : UInt32<GOAL>a.toNat = b.toNat → a = b
<VAR>a : Nat<GOAL>a < UInt32.size → ↑(UInt32.ofNat a).val = a
<VAR>a b : UInt32<VAR>h : a.val ≠ b.val<GOAL>a ≠ b
<VAR>a b : UInt32<GOAL>a ≤ b ↔ a.val ≤ b.val
<VAR>a b : UInt32<VAR>h : a.val = b.val<GOAL>a = b
<VAR>a b : UInt32<GOAL>a % b = { val := a.val % b.val }
<VAR>a b : UInt32<GOAL>a - b = { val := a.val - b.val }
<VAR>a b : UInt32<GOAL>a * b = { val := a.val * b.val }
<VAR>a b : UInt32<VAR>h : a = b<GOAL>a.val = b.val
<VAR>a b : UInt32<GOAL>¬a < b ↔ b ≤ a
<VAR>a b : UInt32<GOAL>a ≤ b ∨ b ≤ a
<VAR>a b : UInt64<GOAL>a.toNat = b.toNat → a = b
<VAR>a b : UInt64<GOAL>a - b = { val := a.val - b.val }
<VAR>a b : UInt64<VAR>h : a < b<GOAL>a ≠ b
<VAR>a b : UInt64<VAR>h : a.val = b.val<GOAL>a = b
<VAR>a b : UInt64<GOAL>(a % b).toNat = a.toNat % b.toNat
<VAR>a b : UInt64<GOAL>a ≤ b ∨ b ≤ a
<VAR>a : UInt64<GOAL>{ val := a.val } = a
<VAR>a b c : UInt64<GOAL>a < b → b < c → a < c
<VAR>a b : UInt64<GOAL>a ≤ b ↔ a.val ≤ b.val
<VAR>a b : UInt64<VAR>h : a = b<GOAL>a.val = b.val
<VAR>a b : UInt64<GOAL>a + b = { val := a.val + b.val }
<VAR>a : Nat<GOAL>a < UInt64.size → ↑(UInt64.ofNat a).val = a
<VAR>m : Nat<VAR>u : UInt64<GOAL>m > 0 → (u % m).toNat < m
<VAR>a b : UInt64<GOAL>(a / b).toNat = a.toNat / b.toNat
<VAR>a b : UInt64<GOAL>¬a ≤ b ↔ b < a
<VAR>a b : UInt64<GOAL>¬a < b ↔ b ≤ a
<VAR>a b : UInt64<GOAL>a < b ↔ a.val < b.val
<VAR>a b : UInt64<VAR>h : a < b<GOAL>¬b < a
<VAR>a b : UInt64<GOAL>a * b = { val := a.val * b.val }
<VAR>a : UInt64<VAR>b : Nat<GOAL>(a.modn b).toNat = a.toNat % b
<VAR>a b : UInt64<VAR>h : 0 < b<GOAL>a % b < b
<VAR>a b : UInt64<GOAL>a % b = { val := a.val % b.val }
<VAR>a b : UInt64<VAR>h : a.val ≠ b.val<GOAL>a ≠ b
<VAR>a b c : UInt64<GOAL>a ≤ b → b ≤ c → a ≤ c
<VAR>a b : USize<GOAL>a ≤ b ↔ a.val ≤ b.val
<VAR>m : Nat<VAR>u : USize<GOAL>m > 0 → (u % m).toNat < m
<VAR>a b : USize<GOAL>a * b = { val := a.val * b.val }
<VAR>a b c : USize<GOAL>a < b → b < c → a < c
<VAR>a b : USize<VAR>h : a.val = b.val<GOAL>a = b
<VAR>a b : USize<VAR>h : a < b<GOAL>¬b < a
<VAR>a : USize<GOAL>{ val := a.val } = a
<VAR>a b : USize<GOAL>a < b ↔ a.val < b.val
<VAR>a b : USize<GOAL>(a % b).toNat = a.toNat % b.toNat
<VAR>a b : USize<VAR>h : 0 < b<GOAL>a % b < b
<VAR>a b : USize<VAR>h : a = b<GOAL>a.val = b.val
<VAR>a b c : USize<GOAL>a ≤ b → b ≤ c → a ≤ c
<VAR>a b : USize<GOAL>a.toNat = b.toNat → a = b
<VAR>a b : USize<GOAL>a ≤ b ∨ b ≤ a
<VAR>a b : USize<GOAL>¬a ≤ b ↔ b < a
<VAR>a b : USize<GOAL>(a / b).toNat = a.toNat / b.toNat
<VAR>a : Nat<GOAL>a < USize.size → ↑(USize.ofNat a).val = a
<VAR>a b : USize<GOAL>a + b = { val := a.val + b.val }
<VAR>a : USize<VAR>b : Nat<GOAL>(a.modn b).toNat = a.toNat % b
<VAR>a b : USize<GOAL>a % b = { val := a.val % b.val }
<VAR>a b : USize<GOAL>¬a < b ↔ b ≤ a
<VAR>a b : USize<VAR>h : a < b<GOAL>a ≠ b
<VAR>a b : USize<VAR>h : a.val ≠ b.val<GOAL>a ≠ b
<VAR>a b : USize<GOAL>a - b = { val := a.val - b.val }
<VAR>α : Type u_1<VAR>i : Nat<VAR>l : List α<GOAL>(List.take i l).length = min i l.length
<VAR>α : Type u_1<VAR>n : Nat<VAR>l : List α<GOAL>(List.take n l).length ≤ n
<VAR>α : Type u_1<VAR>n : Nat<VAR>l : List α<GOAL>(List.take n l).length ≤ l.length
<VAR>n : Nat<GOAL>∀ {α : Type u_1} {l : List α}, n ≤ l.length → (List.take n l).length = n
<VAR>α : Type u_1<VAR>n m : Nat<VAR>l : List α<GOAL>List.take n (List.take m l) = List.take (min n m) l
<VAR>α : Type u_1<VAR>a : α<VAR>n m : Nat<GOAL>List.take n (List.replicate m a) = List.replicate (min n m) a
<VAR>α : Type u_1<VAR>a : α<VAR>n m : Nat<GOAL>List.drop n (List.replicate m a) = List.replicate (m - n) a
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>n : Nat<GOAL>List.take n (l₁ ++ l₂) = List.take n l₁ ++ List.take (n - l₁.length) l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>n : Nat<VAR>h : n ≤ l₁.length<GOAL>List.take n (l₁ ++ l₂) = List.take n l₁
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>i : Nat<GOAL>List.take (l₁.length + i) (l₁ ++ l₂) = l₁ ++ List.take i l₂
<VAR>α : Type u_1<VAR>L : List α<VAR>i j : Nat<VAR>hi : i < L.length<VAR>hj : i < j<GOAL>L[i] = (List.take j L)[i]
<VAR>α : Type u_1<VAR>L : List α<VAR>j i : Nat<VAR>h : i < (List.take j L).length<GOAL>(List.take j L)[i] = L[i]
<VAR>α : Type u_1<VAR>L : List α<VAR>i j : Nat<VAR>hi : i < L.length<VAR>hj : i < j<GOAL>L.get ⟨i, hi⟩ = (List.take j L).get ⟨i, ⋯⟩
<VAR>α : Type u_1<VAR>L : List α<VAR>j : Nat<VAR>i : Fin (List.take j L).length<GOAL>(List.take j L).get i = L.get ⟨↑i, ⋯⟩
<VAR>α : Type u_1<VAR>l : List α<VAR>n m : Nat<VAR>h : n ≤ m<GOAL>(List.take n l)[m]? = none
<VAR>α : Type u_1<VAR>l : List α<VAR>n m : Nat<VAR>h : n ≤ m<GOAL>(List.take n l).get? m = none
<VAR>α : Type u_1<VAR>l : List α<VAR>n m : Nat<GOAL>(List.take n l)[m]? = if m < n then l[m]? else none
<VAR>α : Type u_1<VAR>l : List α<VAR>n m : Nat<GOAL>(List.take n l).get? m = if m < n then l.get? m else none
<VAR>α : Type u_1<VAR>l : List α<VAR>m n : Nat<GOAL>List.take m l = List.take n l ↔ min m l.length = min n l.length
<VAR>α : Type u_1<VAR>l : List α<VAR>m n : Nat<GOAL>List.take (m + n) l = List.take m l ++ List.take n (List.drop m l)
<VAR>α : Type u_1<VAR>n : Nat<VAR>l : List α<VAR>h : n < l.length<GOAL>(List.take n l).dropLast = List.take n.pred l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l : List α<VAR>s₁ s₂ : List β<VAR>h : List.map f l = s₁ ++ s₂<GOAL>∃ l₁ l₂, l = l₁ ++ l₂ ∧ List.map f l₁ = s₁ ∧ List.map f l₂ = s₂
<VAR>α : Type u_1<VAR>l : List α<VAR>h : l ≠ []<VAR>a : α<GOAL>List.drop l.length (a :: l) = [l.getLast h]
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>n : Nat<GOAL>List.drop n (l₁ ++ l₂) = List.drop n l₁ ++ List.drop (n - l₁.length) l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>n : Nat<VAR>h : n ≤ l₁.length<GOAL>List.drop n (l₁ ++ l₂) = List.drop n l₁ ++ l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>i : Nat<GOAL>List.drop (l₁.length + i) (l₁ ++ l₂) = List.drop i l₂
<VAR>α : Type u_1<VAR>L : List α<VAR>i j : Nat<VAR>h : i + j < L.length<GOAL>j < (List.drop i L).length
<VAR>α : Type u_1<VAR>L : List α<VAR>i j : Nat<VAR>h : i + j < L.length<GOAL>L[i + j] = (List.drop i L)[j]
<VAR>α : Type u_1<VAR>L : List α<VAR>i j : Nat<VAR>h : i + j < L.length<GOAL>L.get ⟨i + j, h⟩ = (List.drop i L).get ⟨j, ⋯⟩
<VAR>α : Type u_1<VAR>L : List α<VAR>i j : Nat<VAR>h : j < (List.drop i L).length<GOAL>(List.drop i L)[j] = L[i + j]
<VAR>α : Type u_1<VAR>L : List α<VAR>i : Nat<VAR>j : Fin (List.drop i L).length<GOAL>(List.drop i L).get j = L.get ⟨i + ↑j, ⋯⟩
<VAR>α : Type u_1<VAR>L : List α<VAR>i j : Nat<GOAL>(List.drop i L)[j]? = L[i + j]?
<VAR>α : Type u_1<VAR>L : List α<VAR>i j : Nat<GOAL>(List.drop i L).get? j = L.get? (i + j)
<VAR>α : Type u_1<VAR>l : List α<VAR>n : Nat<VAR>a : α<GOAL>l.set n a = if n < l.length then List.take n l ++ a :: List.drop (n + 1) l else l
<VAR>α : Type u_1<VAR>m n : Nat<VAR>l : List α<GOAL>List.drop n (List.take m l) = List.take (m - n) (List.drop n l)
<VAR>α : Type u_1<VAR>xs : List α<VAR>n : Nat<VAR>h : n ≤ xs.length<GOAL>List.take n xs.reverse = (List.drop (xs.length - n) xs).reverse
<VAR>α : Type u_1<VAR>m : Nat<VAR>n : Nat<VAR>a : α<GOAL>(List.replicate m a).rotateLeft n = List.replicate m a
<VAR>α : Type u_1<VAR>m : Nat<VAR>n : Nat<VAR>a : α<GOAL>(List.replicate m a).rotateRight n = List.replicate m a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>(List.zipWith f l₁ l₂).length = min l₁.length l₂.length
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>∀ {α_1 : Type u_3} {f : α → β → α_1} (l₁ : List α) (l₂ : List β), List.zipWith f l₁ l₂ = List.zipWith f (List.take (min l₁.length l₂.length) l₁) (List.take (min l₁.length l₂.length) l₂)
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>∀ {α_1 : Type u_3} {f : α → β → α_1} {a : α} {b : β} {m n : Nat}, List.zipWith f (List.replicate m a) (List.replicate n b) = List.replicate (min m n) (f a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>(l₁.zip l₂).length = min l₁.length l₂.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>l₁.zip l₂ = (List.take (min l₁.length l₂.length) l₁).zip (List.take (min l₁.length l₂.length) l₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>m n : Nat<GOAL>(List.replicate m a).zip (List.replicate n b) = List.replicate (min m n) (a, b)
<VAR>a : Nat<VAR>xs : List Nat<GOAL>xs.minimum? = some a ↔ a ∈ xs ∧ ∀ (b : Nat), b ∈ xs → a ≤ b
<VAR>a : Nat<VAR>xs : List Nat<GOAL>xs.maximum? = some a ↔ a ∈ xs ∧ ∀ (b : Nat), b ∈ xs → b ≤ a
<VAR>n b a : Nat<GOAL>a < n → b % n < n
<VAR>n : Nat<GOAL>⟨0, ⋯⟩ = 0
<VAR>n : Nat<VAR>i j : Fin n<VAR>h : i ≠ j<GOAL>↑i ≠ ↑j
<VAR>n m : Nat<VAR>i : Fin n<GOAL>m > 0 → ↑(i.modn m) < m
<VAR>n b : Nat<VAR>i : Fin b<VAR>h : b ≤ n<GOAL>↑i < n
<VAR>n : Nat<VAR>i : Fin n<GOAL>0 < n
<VAR>n : Nat<VAR>a b : Fin n<GOAL>↑a = ↑b ↔ a = b
<VAR>n : Nat<VAR>a b : Fin n<VAR>h : a = b<GOAL>↑a = ↑b
<VAR>n : Nat<VAR>a b : Fin n<VAR>h : a ≤ b<GOAL>↑a ≤ ↑b
<VAR>n : Nat<VAR>a b : Fin n<VAR>h : a ≥ b<GOAL>↑b ≤ ↑a
<VAR>n : Nat<VAR>a b : Fin n<VAR>h : a < b<GOAL>↑a + 1 ≤ ↑b
<VAR>n : Nat<VAR>a b : Fin n<VAR>h : a > b<GOAL>↑b + 1 ≤ ↑a
<VAR>n : Nat<VAR>p : Fin n → Prop<GOAL>(Exists fun i => p i) ↔ Exists fun i => Exists fun h => p ⟨i, h⟩
<VAR>α : Type u<VAR>x y : Option α<GOAL>(∀ (z : α), x = some z ↔ y = some z) → x = y
<VAR>α : Type u<VAR>o : Option α<GOAL>o.isNone = true → o = none
<VAR>α : Type u_1<VAR>a : α<VAR>b : Option α<GOAL>a ∈ b ↔ b = some a
<VAR>α : Type u_1<VAR>o : Option α<GOAL>o.isNone = true ↔ o = none
<VAR>α : Type u_1<VAR>a b : α<GOAL>some a = some b ↔ a = b
<GOAL>∀ {α : Type u_1} {a : α}, none.getD a = a
<GOAL>∀ {α : Type u_1} {a b : α}, (some a).getD b = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>Option.map f none = none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>f : α → β<GOAL>Option.map f (some a) = some (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → Option β<GOAL>none.bind f = none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>f : α → Option β<GOAL>(some a).bind f = f a
<GOAL>∀ {α : Type u_1} {p : α → Bool}, Option.all p none = true
<GOAL>∀ {α : Type u_1} {p : α → Bool} {x : α}, Option.all p (some x) = p x
<VAR>α : Type u_1<VAR>Min α<VAR>a b : α<GOAL>min (some a) (some b) = some (min a b)
<VAR>α : Type u_1<VAR>Min α<VAR>a : α<GOAL>min (some a) none = some a
<VAR>α : Type u_1<VAR>Min α<VAR>b : α<GOAL>min none (some b) = some b
<VAR>α : Type u_1<VAR>Min α<GOAL>min none none = none
<VAR>α : Type u_1<VAR>Max α<VAR>a b : α<GOAL>max (some a) (some b) = some (max a b)
<VAR>α : Type u_1<VAR>Max α<VAR>a : α<GOAL>max (some a) none = some a
<VAR>α : Type u_1<VAR>Max α<VAR>b : α<GOAL>max none (some b) = some b
<VAR>α : Type u_1<VAR>Max α<GOAL>max none none = none
<VAR>P : Nat → Sort u_1<VAR>Q : (i : Nat) → P i → Prop<VAR>n : Nat<VAR>f : (i : Fin n) → P ↑i → P (↑i + 1)<VAR>i : Nat<VAR>ubnd : i ≤ n<VAR>s : P i<VAR>init : Q i s<VAR>step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)<GOAL>Q n (Fin.hIterateFrom P f i ubnd s)
<VAR>P : Nat → Sort u_1<VAR>Q : (i : Nat) → P i → Prop<VAR>n : Nat<VAR>f : (i : Fin n) → P ↑i → P (↑i + 1)<VAR>s : P 0<VAR>init : Q 0 s<VAR>step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)<GOAL>Q n (Fin.hIterate P s f)
<VAR>P : Nat → Sort u_1<VAR>state : (i : Nat) → P i<VAR>n : Nat<VAR>f : (i : Fin n) → P ↑i → P (↑i + 1)<VAR>s : P 0<VAR>init : s = state 0<VAR>step : ∀ (i : Fin n), f i (state ↑i) = state (↑i + 1)<GOAL>Fin.hIterate P s f = state n
<VAR>a : Int<GOAL>a.NonNeg ↔ ∃ n, a = ↑n
<VAR>a : Int<GOAL>a.NonNeg → ∃ n, a = ↑n
<VAR>a : Int<GOAL>a.NonNeg ∨ (-a).NonNeg
<VAR>a b : Int<GOAL>a ≤ b ↔ (b - a).NonNeg
<VAR>a b : Int<GOAL>a < b ↔ a + 1 ≤ b
<VAR>a b : Int<VAR>n : Nat<VAR>h : b - a = ↑n<GOAL>a ≤ b
<VAR>a b : Int<VAR>n : Nat<VAR>h : a + ↑n = b<GOAL>a ≤ b
<VAR>a b : Int<VAR>h : a ≤ b<GOAL>∃ n, b - a = ↑n
<VAR>a b : Int<VAR>h : a ≤ b<GOAL>∃ n, a + ↑n = b
<VAR>a b : Int<GOAL>a ≤ b ∨ b ≤ a
<VAR>m n : Nat<GOAL>↑m ≤ ↑n ↔ m ≤ n
<VAR>n : Nat<GOAL>0 ≤ ↑n
<VAR>a : Int<VAR>h : 0 ≤ a<GOAL>∃ n, a = ↑n
<VAR>a : Int<VAR>h : 0 < a<GOAL>∃ n, a = ↑n.succ
<VAR>a : Int<VAR>n : Nat<GOAL>a < a + ↑n.succ
<VAR>a b : Int<VAR>n : Nat<VAR>h : a + ↑n.succ = b<GOAL>a < b
<VAR>a b : Int<VAR>h : a < b<GOAL>∃ n, a + ↑n.succ = b
<VAR>n m : Nat<GOAL>↑n < ↑m ↔ n < m
<VAR>n : Nat<GOAL>0 < ↑n ↔ 0 < n
<VAR>n : Nat<GOAL>0 < ↑n.succ
<VAR>a b c : Int<VAR>h₁ : a ≤ b<VAR>h₂ : b ≤ c<GOAL>a ≤ c
<VAR>a b : Int<VAR>h₁ : a ≤ b<VAR>h₂ : b ≤ a<GOAL>a = b
<VAR>a b : Int<VAR>h : a < b<GOAL>a ≠ b
<VAR>a b : Int<VAR>h : b < a<GOAL>a ≠ b
<VAR>a b : Int<VAR>h : a < b<GOAL>a ≤ b
<VAR>a b : Int<GOAL>a < b ↔ a ≤ b ∧ a ≠ b
<VAR>a b : Int<GOAL>a < b ↔ a ≤ b ∧ ¬b ≤ a
<VAR>a b : Int<VAR>h : ¬a ≤ b<GOAL>b < a
<VAR>a b : Int<VAR>h : b < a<GOAL>¬a ≤ b
<VAR>a b : Int<GOAL>¬a ≤ b ↔ b < a
<VAR>a b : Int<GOAL>¬a < b ↔ b ≤ a
<VAR>a b : Int<GOAL>a < b ∨ a = b ∨ b < a
<VAR>a b : Int<GOAL>a ≠ b ↔ a < b ∨ b < a
<VAR>a b : Int<GOAL>a ≠ b → a < b ∨ b < a
<VAR>x y : Int<GOAL>x = y ↔ x ≤ y ∧ y ≤ x
<VAR>a b c : Int<VAR>h₁ : a ≤ b<VAR>h₂ : b < c<GOAL>a < c
<VAR>a b c : Int<VAR>h₁ : a < b<VAR>h₂ : b ≤ c<GOAL>a < c
<VAR>a b c : Int<VAR>h₁ : a < b<VAR>h₂ : b < c<GOAL>a < c
<VAR>n m : Int<GOAL>min n m = if n ≤ m then n else m
<VAR>n m : Int<GOAL>max n m = if n ≤ m then m else n
<VAR>a b : Int<VAR>h : a ≤ b<GOAL>min a b = a
<VAR>a b : Int<VAR>h : b ≤ a<GOAL>min a b = b
<VAR>a b c : Int<GOAL>a ≤ min b c ↔ a ≤ b ∧ a ≤ c
<VAR>a b c : Int<GOAL>max a b ≤ c ↔ a ≤ c ∧ b ≤ c
<VAR>a b : Int<VAR>h : a ≤ b<GOAL>max a b = b
<VAR>a b : Int<VAR>h : b ≤ a<GOAL>max a b = a
<VAR>a : Int<VAR>h : 0 ≤ a<GOAL>a = ↑a.natAbs
<VAR>a : Int<GOAL>a ≤ ↑a.natAbs
<VAR>n : Nat<GOAL>Int.negSucc n < 0
<VAR>n : Nat<GOAL>0 ≤ Int.negSucc n ↔ False
<VAR>a b : Int<VAR>h : a ≤ b<VAR>c : Int<GOAL>c + a ≤ c + b
<VAR>a b : Int<VAR>h : a < b<VAR>c : Int<GOAL>c + a < c + b
<VAR>a b : Int<VAR>h : a ≤ b<VAR>c : Int<GOAL>a + c ≤ b + c
<VAR>a b : Int<VAR>h : a < b<VAR>c : Int<GOAL>a + c < b + c
<VAR>a b c : Int<VAR>h : a + b ≤ a + c<GOAL>b ≤ c
<VAR>a b c : Int<VAR>h : a + b ≤ c + b<GOAL>a ≤ c
<VAR>b c : Int<VAR>a : Int<GOAL>a + b ≤ a + c ↔ b ≤ c
<VAR>a b : Int<VAR>c : Int<GOAL>a + c ≤ b + c ↔ a ≤ b
<VAR>a b c d : Int<VAR>h₁ : a ≤ b<VAR>h₂ : c ≤ d<GOAL>a + c ≤ b + d
<VAR>a b : Int<VAR>h : 0 ≤ b<GOAL>a ≤ a + b
<VAR>a b : Int<VAR>h : 0 ≤ b<GOAL>a ≤ b + a
<VAR>a b : Int<VAR>h : a ≤ b<GOAL>-b ≤ -a
<VAR>a b : Int<VAR>h : -b ≤ -a<GOAL>a ≤ b
<VAR>a : Int<VAR>h : 0 ≤ a<GOAL>-a ≤ 0
<VAR>a : Int<VAR>h : a ≤ 0<GOAL>0 ≤ -a
<VAR>a b : Int<VAR>h : a < b<GOAL>-b < -a
<VAR>a : Int<VAR>h : 0 < a<GOAL>-a < 0
<VAR>a : Int<VAR>h : a < 0<GOAL>0 < -a
<VAR>a b : Int<VAR>h : b ≤ a<GOAL>0 ≤ a - b
<VAR>a b : Int<VAR>h : 0 ≤ a - b<GOAL>b ≤ a
<VAR>a b : Int<VAR>h : b < a<GOAL>0 < a - b
<VAR>a b : Int<VAR>h : 0 < a - b<GOAL>b < a
<VAR>a b c : Int<VAR>h : a ≤ b + c<GOAL>a - b ≤ c
<VAR>a : Int<VAR>b : Int<VAR>h : 0 ≤ b<GOAL>a - b ≤ a
<VAR>a : Int<VAR>b : Int<VAR>h : 0 < b<GOAL>a - b < a
<VAR>a b : Int<VAR>H : a < b<GOAL>a + 1 ≤ b
<VAR>a b : Int<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>0 ≤ a * b
<VAR>a b : Int<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>0 < a * b
<VAR>a b c : Int<VAR>h₁ : a < b<VAR>h₂ : 0 < c<GOAL>c * a < c * b
<VAR>a b c : Int<VAR>h₁ : a < b<VAR>h₂ : 0 < c<GOAL>a * c < b * c
<VAR>a b c : Int<VAR>h₁ : a ≤ b<VAR>h₂ : 0 ≤ c<GOAL>c * a ≤ c * b
<VAR>a b c : Int<VAR>h₁ : a ≤ b<VAR>h₂ : 0 ≤ c<GOAL>a * c ≤ b * c
<VAR>a b c d : Int<VAR>hac : a ≤ c<VAR>hbd : b ≤ d<VAR>nn_b : 0 ≤ b<VAR>nn_c : 0 ≤ c<GOAL>a * b ≤ c * d
<VAR>a b : Int<VAR>ha : 0 ≤ a<VAR>hb : b ≤ 0<GOAL>a * b ≤ 0
<VAR>a b : Int<VAR>ha : a ≤ 0<VAR>hb : 0 ≤ b<GOAL>a * b ≤ 0
<VAR>a b c : Int<VAR>h : b ≤ a<VAR>hc : c ≤ 0<GOAL>a * c ≤ b * c
<VAR>a b c : Int<VAR>ha : a ≤ 0<VAR>h : c ≤ b<GOAL>a * b ≤ a * c
<VAR>n : Nat<GOAL>(↑n).natAbs = n
<VAR>n : Nat<GOAL>(Int.negSucc n).natAbs = n.succ
<VAR>a : Int<GOAL>a.natAbs = 0 ↔ a = 0
<VAR>a : Int<GOAL>0 < a.natAbs ↔ a ≠ 0
<VAR>a : Int<GOAL>(-a).natAbs = a.natAbs
<VAR>a : Int<GOAL>a = ↑a.natAbs ∨ a = -↑a.natAbs
<VAR>n : Nat<GOAL>(Int.negOfNat n).natAbs = n
<VAR>a b : Int<GOAL>(a * b).natAbs = a.natAbs * b.natAbs
<VAR>a b : Int<GOAL>a.natAbs = b.natAbs ↔ a = b ∨ a = -b
<VAR>a : Int<VAR>H : 0 ≤ a<GOAL>↑a.natAbs = a
<VAR>a : Int<VAR>H : a ≤ 0<GOAL>↑a.natAbs = -a
<VAR>a : Int<GOAL>↑a.toNat = max a 0
<VAR>a : Int<VAR>h : 0 ≤ a<GOAL>↑a.toNat = a
<VAR>n : Nat<GOAL>(↑n).toNat = n
<VAR>n : Nat<GOAL>(↑n + 1).toNat = n + 1
<VAR>a : Int<GOAL>a ≤ ↑a.toNat
<VAR>n : Nat<VAR>z : Int<VAR>h : 0 ≤ z<GOAL>n ≤ z.toNat ↔ ↑n ≤ z
<VAR>n : Nat<VAR>z : Int<VAR>h : 0 ≤ z<GOAL>z.toNat < n ↔ z < ↑n
<VAR>a b : Int<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>(a + b).toNat = a.toNat + b.toNat
<VAR>a : Int<VAR>ha : 0 ≤ a<VAR>n : Nat<GOAL>(a + ↑n).toNat = a.toNat + n
<VAR>i : Int<GOAL>(i - 1).toNat = i.toNat - 1
<VAR>n : Int<GOAL>↑n.toNat - ↑(-n).toNat = n
<VAR>n : Int<GOAL>n.toNat + (-n).toNat = n.natAbs
<VAR>n : Nat<GOAL>(-↑n).toNat = 0
<VAR>a : Int<VAR>n : Nat<GOAL>a.toNat' = some n ↔ a = ↑n
<VAR>a b : Int<GOAL>¬a ≤ b → b ≤ a
<VAR>n : Nat<GOAL>0 < Int.negSucc n ↔ False
<VAR>a : Int<GOAL>a < 0 → ∃ n, a = Int.negSucc n
<VAR>a b c : Int<VAR>h : a + b < a + c<GOAL>b < c
<VAR>a b c : Int<VAR>h : a + b < c + b<GOAL>a < c
<VAR>b c : Int<VAR>a : Int<GOAL>a + b < a + c ↔ b < c
<VAR>a b : Int<VAR>c : Int<GOAL>a + c < b + c ↔ a < b
<VAR>a b c d : Int<VAR>h₁ : a < b<VAR>h₂ : c < d<GOAL>a + c < b + d
<VAR>a b c d : Int<VAR>h₁ : a ≤ b<VAR>h₂ : c < d<GOAL>a + c < b + d
<VAR>a b c d : Int<VAR>h₁ : a < b<VAR>h₂ : c ≤ d<GOAL>a + c < b + d
<VAR>a : Int<VAR>b : Int<VAR>h : 0 < b<GOAL>a < a + b
<VAR>a : Int<VAR>b : Int<VAR>h : 0 < b<GOAL>a < b + a
<VAR>a b : Int<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>0 ≤ a + b
<VAR>a b : Int<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>0 < a + b
<VAR>a b : Int<VAR>ha : 0 < a<VAR>hb : 0 ≤ b<GOAL>0 < a + b
<VAR>a b : Int<VAR>ha : 0 ≤ a<VAR>hb : 0 < b<GOAL>0 < a + b
<VAR>a b : Int<VAR>ha : a ≤ 0<VAR>hb : b ≤ 0<GOAL>a + b ≤ 0
<VAR>a b : Int<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>a + b < 0
<VAR>a b : Int<VAR>ha : a < 0<VAR>hb : b ≤ 0<GOAL>a + b < 0
<VAR>a b : Int<VAR>ha : a ≤ 0<VAR>hb : b < 0<GOAL>a + b < 0
<VAR>a b c : Int<VAR>hbc : b ≤ c<VAR>ha : 0 < a<GOAL>b < c + a
<VAR>a b : Int<GOAL>a + 1 ≤ b ↔ a < b
<VAR>a b : Int<GOAL>a < b + 1 ↔ a ≤ b
<VAR>n : Nat<GOAL>0 < ↑n + 1
<VAR>a b : Int<VAR>h : a ≤ b<GOAL>a ≤ b + 1
<VAR>a : Int<VAR>h : -a ≤ 0<GOAL>0 ≤ a
<VAR>a : Int<VAR>h : 0 ≤ -a<GOAL>a ≤ 0
<VAR>a b : Int<VAR>h : -b < -a<GOAL>a < b
<VAR>a : Int<VAR>h : -a < 0<GOAL>0 < a
<VAR>a : Int<VAR>h : 0 < -a<GOAL>a < 0
<VAR>a b : Int<VAR>h : a ≤ -b<GOAL>b ≤ -a
<VAR>a b : Int<VAR>h : -a ≤ b<GOAL>-b ≤ a
<VAR>a b : Int<VAR>h : a < -b<GOAL>b < -a
<VAR>a b : Int<VAR>h : -a < b<GOAL>-b < a
<VAR>a b : Int<VAR>h : a ≤ b<GOAL>a - b ≤ 0
<VAR>a b : Int<VAR>h : a - b ≤ 0<GOAL>a ≤ b
<VAR>a b : Int<VAR>h : a < b<GOAL>a - b < 0
<VAR>a b : Int<VAR>h : a - b < 0<GOAL>a < b
<VAR>a b c : Int<VAR>h : b ≤ -a + c<GOAL>a + b ≤ c
<VAR>a b c : Int<VAR>h : a + b ≤ c<GOAL>b ≤ -a + c
<VAR>a b c : Int<VAR>h : b ≤ c - a<GOAL>a + b ≤ c
<VAR>a b c : Int<VAR>h : a + b ≤ c<GOAL>b ≤ c - a
<VAR>a b c : Int<VAR>h : a ≤ c - b<GOAL>a + b ≤ c
<VAR>a b c : Int<VAR>h : a + b ≤ c<GOAL>a ≤ c - b
<VAR>a b c : Int<VAR>h : -b + a ≤ c<GOAL>a ≤ b + c
<VAR>a b c : Int<VAR>h : a ≤ b + c<GOAL>-b + a ≤ c
<VAR>a b c : Int<VAR>h : a - b ≤ c<GOAL>a ≤ b + c
<VAR>a b c : Int<VAR>h : a - c ≤ b<GOAL>a ≤ b + c
<VAR>a b c : Int<VAR>h : a ≤ b + c<GOAL>a - c ≤ b
<VAR>a b c : Int<VAR>h : -c + a ≤ b<GOAL>a ≤ b + c
<VAR>a b c : Int<VAR>h : a ≤ b + c<GOAL>-c + a ≤ b
<VAR>a b c : Int<VAR>h : -a ≤ b - c<GOAL>c ≤ a + b
<VAR>a b c : Int<VAR>h : c ≤ a + b<GOAL>-a ≤ b - c
<VAR>a b c : Int<VAR>h : -b ≤ a - c<GOAL>c ≤ a + b
<VAR>a b c : Int<VAR>h : c ≤ a + b<GOAL>-b ≤ a - c
<VAR>a b c : Int<VAR>h : a - b ≤ c<GOAL>a - c ≤ b
<VAR>a b : Int<VAR>h : a ≤ b<VAR>c : Int<GOAL>c - b ≤ c - a
<VAR>a b : Int<VAR>h : a ≤ b<VAR>c : Int<GOAL>a - c ≤ b - c
<VAR>a b c d : Int<VAR>hab : a ≤ b<VAR>hcd : c ≤ d<GOAL>a - d ≤ b - c
<VAR>a b c : Int<VAR>h : b < -a + c<GOAL>a + b < c
<VAR>a b c : Int<VAR>h : a + b < c<GOAL>b < -a + c
<VAR>a b c : Int<VAR>h : b < c - a<GOAL>a + b < c
<VAR>a b c : Int<VAR>h : a + b < c<GOAL>b < c - a
<VAR>a b c : Int<VAR>h : a < c - b<GOAL>a + b < c
<VAR>a b c : Int<VAR>h : a + b < c<GOAL>a < c - b
<VAR>a b c : Int<VAR>h : -b + a < c<GOAL>a < b + c
<VAR>a b c : Int<VAR>h : a < b + c<GOAL>-b + a < c
<VAR>a b c : Int<VAR>h : a - b < c<GOAL>a < b + c
<VAR>a b c : Int<VAR>h : a < b + c<GOAL>a - b < c
<VAR>a b c : Int<VAR>h : a - c < b<GOAL>a < b + c
<VAR>a b c : Int<VAR>h : a < b + c<GOAL>a - c < b
<VAR>a b c : Int<VAR>h : -c + a < b<GOAL>a < b + c
<VAR>a b c : Int<VAR>h : a < b + c<GOAL>-c + a < b
<VAR>a b c : Int<VAR>h : -a < b - c<GOAL>c < a + b
<VAR>a b c : Int<VAR>h : c < a + b<GOAL>-a < b - c
<VAR>a b c : Int<VAR>h : -b < a - c<GOAL>c < a + b
<VAR>a b c : Int<VAR>h : c < a + b<GOAL>-b < a - c
<VAR>a b c : Int<GOAL>a + b < c ↔ a < -b + c