LessnessRandomness

--- 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

LessnessRandomness

import Mathlib

inductive IndGraph: Nat → Type where
  | Empty: IndGraph 0
  | Cons: ∀ {n}, Set (Fin n) → IndGraph n → IndGraph (n + 1)

def IndGraph.adjacent {n} (G: IndGraph n): Fin n → Fin n → Prop :=
  fun x y => match G with
             | IndGraph.Empty => False
             | @IndGraph.Cons m S Gₘ =>