LessnessRandomness

import Mathlib


def rep_div (n f : ℕ) : ℕ :=
  if (1 ≤ n ∧ 2 ≤ f ∧ f ∣ n)
  then rep_div (n / f) f
  else n
termination_by n
decreasing_by exact Nat.div_lt_self (by lia) (by lia)

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

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