2 more proofs from The Mechanics

Stream: new members

[Michael Bucko]

Wrote two more proofs from The Mechanics Of Proof. I'd appreciate your feedback.

2 proofs

import Mathlib
import Lean

example {a n : ℤ} : n ∣ a ↔ a ≡ 0 [ZMOD n] := by
  constructor
  · intro h
    obtain ⟨k, hk⟩ := h
    rw [hk]
    simp [Int.modEq_zero_iff_dvd]
  · intro h
    rw [Int.modEq_zero_iff_dvd] at h
    exact h

example : ¬ 3 ∣ 13 := by
  intro H
  obtain ⟨k, hk⟩ := H
  obtain h4 | h5 := le_or_lt k 4
  ·
    have : 13 ≤ 3 * 4 := by rw [hk]; exact Nat.mul_le_mul_left 3 h4
    linarith
  ·
    have : 13 ≥ 3 * 5 := by rw [hk]; exact Nat.mul_le_mul_left 3 (Nat.succ_le_iff.mp h5)
    linarith