nat_mod.lean

import 
  tactic
  data.int.basic tactic.omega 


def mod_nat : nat → nat → nat
| addr p :=
    if h₁ : p = 0 then 
       0
    else 
      if h₂ : addr < p then
         addr
      else
        have addr - p < addr, by omega, 
        mod_nat (addr - p) p 


lemma mod_nat_proof : ∀ (addr p: ℕ), p > 0 → mod_nat addr p < p
| addr p :=
    if h₁ : p = 0 then 
      begin 
        intros, rw h₁ at a, exact (mul_lt_mul_right a).mp a, 
      end
    else 
      if h₂ : addr < p then
        begin
          intros, rw mod_nat,
          rwa [if_neg h₁, if_pos h₂]
        end  
      else
        begin 
          intro a,
          have H₁ : addr >= p := by exact not_lt.mp h₂, 
          have H₂ : addr - p >= 0 := by exact bot_le,
          have H₃ : addr - p < addr := by exact nat.sub_lt_of_pos_le p addr a H₁,
          specialize (mod_nat_proof (addr - p) p a),
          rw mod_nat, rwa [if_neg h₁, if_neg h₂],
        end