Skip to content

Instantly share code, notes, and snippets.

--- This is adapted solution to 3rd exercise from Project Euler
--- from https://codereview.stackexchange.com/questions/74587/project-euler-3-in-java/74792#74792
--- by Altinak
import Mathlib
lemma div_at_least_one {n f: ℕ} (Hn: 1 ≤ n) (Hf: 2 ≤ f) (H: f ∣ n): 1 ≤ n / f := by
cases H with | intro w h =>
rw [h, Nat.mul_div_cancel_left] <;> nlinarith