refactor(data/int/basic): weaken hypotheses for int.induction_on

leanprover-community · Apr 4, 2019 · 665dede · 665dede
1 parent 07aa1e3
commit 665dede
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/data/int/basic.lean b/src/data/int/basic.lean
@@ -95,7 +95,7 @@ theorem le_sub_one_iff {a b : ℤ} : a ≤ b - 1 ↔ a < b :=
 le_sub_iff_add_le
 
 @[elab_as_eliminator] protected lemma induction_on {p : ℤ → Prop}
-  (i : ℤ) (hz : p 0) (hp : ∀i, p i → p (i + 1)) (hn : ∀i, p i → p (i - 1)) : p i :=
+  (i : ℤ) (hz : p 0) (hp : ∀i : ℕ, p i → p (i + 1)) (hn : ∀i : ℕ, p (-i) → p (-i - 1)) : p i :=
 begin
   induction i,
   { induction i,