import data.nat data.prod logic.wf_k
open nat well_founded decidable prod eq.ops

-- Auxiliary lemma used to justify recursive call
private definition lt_aux {x y : nat} (H : 0 < y ∧ y ≤ x) : x - y < x :=
and.rec_on H (λ ypos ylex,
  sub.lt (lt_le.trans ypos ylex) ypos)

definition wdiv.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat :=
dif 0 < y ∧ y ≤ x then (λ Hp, f (x - y) (lt_aux Hp) y + 1) else (λ Hn, zero)

definition wdiv (x y : nat) :=
fix wdiv.F x y

theorem wdiv_def (x y : nat) : wdiv x y = if 0 < y ∧ y ≤ x then wdiv (x - y) y + 1 else 0 :=
congr_fun (well_founded.fix_eq wdiv.F x) y

example : wdiv 5 2 = 2 :=
rfl

example : wdiv 9 3 = 3 :=
rfl

-- There is a little bit of cheating in the definition above.
-- I avoid the packing/unpacking into tuples.
-- The actual definitional package would not do that.
-- It will always pack things.

definition pair_nat.lt    := lex lt lt  -- Could also be (lex lt empty_rel)
definition pair_nat.lt.wf [instance] : well_founded pair_nat.lt :=
prod.lex.wf lt.wf lt.wf
infixl `≺`:50 := pair_nat.lt

-- Recursive lemma used to justify recursive call
definition plt_aux (x y : nat) (H : 0 < y ∧ y ≤ x) : (x - y, y) ≺ (x, y) :=
!lex.left (lt_aux H)

definition pdiv.F (p₁ : nat × nat) : (Π p₂ : nat × nat, p₂ ≺ p₁ → nat) → nat :=
prod.cases_on p₁ (λ x y f,
  dif 0 < y ∧ y ≤ x then (λ Hp, f (x - y, y) (plt_aux x y Hp) + 1) else (λ Hnp, zero))

definition pdiv (x y : nat) :=
fix pdiv.F (x, y)

theorem pdiv_def (x y : nat) : pdiv x y = if 0 < y ∧ y ≤ x then pdiv (x - y) y + 1 else zero :=
well_founded.fix_eq pdiv.F (x, y)

example : pdiv 17 2 = 8 :=
rfl