Rename induction hypotheses in Sum.lean for consistency

Changes

1 changed files (+2/-2)

• Sum.lean
  • @@ -43,7 +43,7 @@ lemma exp_larger (n : ℕ) (h : 3 ≤ n) : 2 * (n - 2) ≤ 2 ^ (n - 1) := by
    induction h with | refl => trivial - | step a a_ih => + | step h ih => grind [mul_pow_sub_one] -- Another similar lemma
  • @@ -52,7 +52,7 @@ lemma exp_larger' (n : ℕ) (h : 5 ≤ n) : n * (n - 1) * (n - 2) < (2 * n - 3)
    induction h with | refl => trivial - | step a a_ih => + | step h ih => rename_i m suffices (m + 1) * (m * (m - 1)) ≤ 2 * (m - 2) * (m * (m - 1)) by grind apply Nat.mul_le_mul_right (m * (m - 1))