[GOAL]
n : ℕ+
⊢ 1 + natPred n = ↑n
[PROOFSTEP]
rw [natPred, add_tsub_cancel_iff_le.mpr <| show 1 ≤ (n : ℕ) from n.2]
[GOAL]
a b : ℕ+
⊢ ↑(a - b) = if b < a then ↑a - ↑b else 1
[PROOFSTEP]
change (toPNat' _ : ℕ) = ite _ _ _
[GOAL]
a b : ℕ+
⊢ ↑(toPNat' (↑a - ↑b)) = if b < a then ↑a - ↑b else 1
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
a b : ℕ+
h : b < a
⊢ ↑(toPNat' (↑a - ↑b)) = ↑a - ↑b
[PROOFSTEP]
exact toPNat'_coe (tsub_pos_of_lt h)
[GOAL]
case neg
a b : ℕ+
h : ¬b < a
⊢ ↑(toPNat' (↑a - ↑b)) = 1
[PROOFSTEP]
rw [tsub_eq_zero_iff_le.mpr (le_of_not_gt h : (a : ℕ) ≤ b)]
[GOAL]
case neg
a b : ℕ+
h : ¬b < a
⊢ ↑(toPNat' 0) = 1
[PROOFSTEP]
rfl
[GOAL]
a b : ℕ+
h : a < b
⊢ ↑(a + (b - a)) = ↑b
[PROOFSTEP]
rw [add_coe, sub_coe, if_pos h]
[GOAL]
a b : ℕ+
h : a < b
⊢ ↑a + (↑b - ↑a) = ↑b
[PROOFSTEP]
exact add_tsub_cancel_of_le h.le
[GOAL]
n : ℕ
property✝ : 0 < n + 2
x✝ : { val := n + 2, property := property✝ } ≠ 1
⊢ 0 < n + 1
[PROOFSTEP]
simp
[GOAL]
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
⊢ p a
[PROOFSTEP]
apply strongInductionOn a
[GOAL]
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
⊢ (k : ℕ+) → ((m : ℕ+) → m < k → p m) → p k
[PROOFSTEP]
rintro ⟨k, kprop⟩ hk
[GOAL]
case mk
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
k : ℕ
kprop : 0 < k
hk : (m : ℕ+) → m < { val := k, property := kprop } → p m
⊢ p { val := k, property := kprop }
[PROOFSTEP]
cases' k with k
[GOAL]
case mk.zero
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
kprop : 0 < zero
hk : (m : ℕ+) → m < { val := zero, property := kprop } → p m
⊢ p { val := zero, property := kprop }
[PROOFSTEP]
exact (lt_irrefl 0 kprop).elim
[GOAL]
case mk.succ
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
k : ℕ
kprop : 0 < succ k
hk : (m : ℕ+) → m < { val := succ k, property := kprop } → p m
⊢ p { val := succ k, property := kprop }
[PROOFSTEP]
cases' k with k
[GOAL]
case mk.succ.zero
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
kprop : 0 < succ zero
hk : (m : ℕ+) → m < { val := succ zero, property := kprop } → p m
⊢ p { val := succ zero, property := kprop }
[PROOFSTEP]
exact hz
[GOAL]
case mk.succ.succ
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
k : ℕ
kprop : 0 < succ (succ k)
hk : (m : ℕ+) → m < { val := succ (succ k), property := kprop } → p m
⊢ p { val := succ (succ k), property := kprop }
[PROOFSTEP]
exact hi ⟨k.succ, Nat.succ_pos _⟩ fun m hm => hk _ (lt_succ_iff.2 hm)
[GOAL]
n : ℕ+
p : ℕ+ → Sort u_1
p1 : p 1
hp : (n : ℕ+) → p n → p (n + 1)
⊢ p n
[PROOFSTEP]
rcases n with ⟨n, h⟩
[GOAL]
case mk
p : ℕ+ → Sort u_1
p1 : p 1
hp : (n : ℕ+) → p n → p (n + 1)
n : ℕ
h : 0 < n
⊢ p { val := n, property := h }
[PROOFSTEP]
induction' n with n IH
[GOAL]
case mk.zero
p : ℕ+ → Sort u_1
p1 : p 1
hp : (n : ℕ+) → p n → p (n + 1)
n : ℕ
h✝ : 0 < n
h : 0 < zero
⊢ p { val := zero, property := h }
[PROOFSTEP]
exact absurd h (by decide)
[GOAL]
p : ℕ+ → Sort u_1
p1 : p 1
hp : (n : ℕ+) → p n → p (n + 1)
n : ℕ
h✝ : 0 < n
h : 0 < zero
⊢ ¬0 < zero
[PROOFSTEP]
decide
[GOAL]
case mk.succ
p : ℕ+ → Sort u_1
p1 : p 1
hp : (n : ℕ+) → p n → p (n + 1)
n✝ : ℕ
h✝ : 0 < n✝
n : ℕ
IH : (h : 0 < n) → p { val := n, property := h }
h : 0 < succ n
⊢ p { val := succ n, property := h }
[PROOFSTEP]
cases' n with n
[GOAL]
case mk.succ.zero
p : ℕ+ → Sort u_1
p1 : p 1
hp : (n : ℕ+) → p n → p (n + 1)
n : ℕ
h✝ : 0 < n
IH : (h : 0 < zero) → p { val := zero, property := h }
h : 0 < succ zero
⊢ p { val := succ zero, property := h }
[PROOFSTEP]
exact p1
[GOAL]
case mk.succ.succ
p : ℕ+ → Sort u_1
p1 : p 1
hp : (n : ℕ+) → p n → p (n + 1)
n✝ : ℕ
h✝ : 0 < n✝
n : ℕ
IH : (h : 0 < succ n) → p { val := succ n, property := h }
h : 0 < succ (succ n)
⊢ p { val := succ (succ n), property := h }
[PROOFSTEP]
exact hp _ (IH n.succ_pos)
[GOAL]
n : ℕ+
p : ℕ+ → Sort u_1
p1 : p 1
hp : (n : ℕ+) → p n → p (n + 1)
⊢ recOn (n + 1) p1 hp = hp n (recOn n p1 hp)
[PROOFSTEP]
cases' n with n h
[GOAL]
case mk
p : ℕ+ → Sort u_1
p1 : p 1
hp : (n : ℕ+) → p n → p (n + 1)
n : ℕ
h : 0 < n
⊢ recOn ({ val := n, property := h } + 1) p1 hp =
    hp { val := n, property := h } (recOn { val := n, property := h } p1 hp)
[PROOFSTEP]
cases n <;> [exact absurd h (by decide); rfl]
[GOAL]
case mk
p : ℕ+ → Sort u_1
p1 : p 1
hp : (n : ℕ+) → p n → p (n + 1)
n : ℕ
h : 0 < n
⊢ recOn ({ val := n, property := h } + 1) p1 hp =
    hp { val := n, property := h } (recOn { val := n, property := h } p1 hp)
[PROOFSTEP]
cases n
[GOAL]
case mk.zero
p : ℕ+ → Sort u_1
p1 : p 1
hp : (n : ℕ+) → p n → p (n + 1)
h : 0 < zero
⊢ recOn ({ val := zero, property := h } + 1) p1 hp =
    hp { val := zero, property := h } (recOn { val := zero, property := h } p1 hp)
[PROOFSTEP]
exact absurd h (by decide)
[GOAL]
p : ℕ+ → Sort u_1
p1 : p 1
hp : (n : ℕ+) → p n → p (n + 1)
h : 0 < zero
⊢ ¬0 < zero
[PROOFSTEP]
decide
[GOAL]
case mk.succ
p : ℕ+ → Sort u_1
p1 : p 1
hp : (n : ℕ+) → p n → p (n + 1)
n✝ : ℕ
h : 0 < succ n✝
⊢ recOn ({ val := succ n✝, property := h } + 1) p1 hp =
    hp { val := succ n✝, property := h } (recOn { val := succ n✝, property := h } p1 hp)
[PROOFSTEP]
rfl
[GOAL]
k : ℕ+
q : ℕ
x✝ : ¬(0 = 0 ∧ q + 1 = 0)
⊢ ↑(modDivAux k 0 (q + 1)).fst + ↑k * (modDivAux k 0 (q + 1)).snd = 0 + ↑k * (q + 1)
[PROOFSTEP]
change (k : ℕ) + (k : ℕ) * (q + 1).pred = 0 + (k : ℕ) * (q + 1)
[GOAL]
k : ℕ+
q : ℕ
x✝ : ¬(0 = 0 ∧ q + 1 = 0)
⊢ ↑k + ↑k * pred (q + 1) = 0 + ↑k * (q + 1)
[PROOFSTEP]
rw [Nat.pred_succ, Nat.mul_succ, zero_add, add_comm]
[GOAL]
m k : ℕ+
⊢ ↑(mod m k) + ↑k * div m k = ↑m
[PROOFSTEP]
let h₀ := Nat.mod_add_div (m : ℕ) (k : ℕ)
[GOAL]
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
⊢ ↑(mod m k) + ↑k * div m k = ↑m
[PROOFSTEP]
have : ¬((m : ℕ) % (k : ℕ) = 0 ∧ (m : ℕ) / (k : ℕ) = 0) :=
  by
  rintro ⟨hr, hq⟩
  rw [hr, hq, mul_zero, zero_add] at h₀ 
  exact (m.ne_zero h₀.symm).elim
[GOAL]
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
⊢ ¬(↑m % ↑k = 0 ∧ ↑m / ↑k = 0)
[PROOFSTEP]
rintro ⟨hr, hq⟩
[GOAL]
case intro
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
hr : ↑m % ↑k = 0
hq : ↑m / ↑k = 0
⊢ False
[PROOFSTEP]
rw [hr, hq, mul_zero, zero_add] at h₀ 
[GOAL]
case intro
m k : ℕ+
h₀ : 0 = ↑m
hr : ↑m % ↑k = 0
hq : ↑m / ↑k = 0
⊢ False
[PROOFSTEP]
exact (m.ne_zero h₀.symm).elim
[GOAL]
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
this : ¬(↑m % ↑k = 0 ∧ ↑m / ↑k = 0)
⊢ ↑(mod m k) + ↑k * div m k = ↑m
[PROOFSTEP]
have := modDivAux_spec k ((m : ℕ) % (k : ℕ)) ((m : ℕ) / (k : ℕ)) this
[GOAL]
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
this✝ : ¬(↑m % ↑k = 0 ∧ ↑m / ↑k = 0)
this : ↑(modDivAux k (↑m % ↑k) (↑m / ↑k)).fst + ↑k * (modDivAux k (↑m % ↑k) (↑m / ↑k)).snd = ↑m % ↑k + ↑k * (↑m / ↑k)
⊢ ↑(mod m k) + ↑k * div m k = ↑m
[PROOFSTEP]
exact this.trans h₀
[GOAL]
m k : ℕ+
⊢ ↑(mod m k) + div m k * ↑k = ↑m
[PROOFSTEP]
rw [mul_comm]
[GOAL]
m k : ℕ+
⊢ ↑(mod m k) + ↑k * div m k = ↑m
[PROOFSTEP]
exact mod_add_div _ _
[GOAL]
m k : ℕ+
⊢ div m k * ↑k + ↑(mod m k) = ↑m
[PROOFSTEP]
rw [mul_comm]
[GOAL]
m k : ℕ+
⊢ ↑k * div m k + ↑(mod m k) = ↑m
[PROOFSTEP]
exact div_add_mod _ _
[GOAL]
m k : ℕ+
⊢ mod m k ≤ m ∧ mod m k ≤ k
[PROOFSTEP]
change (mod m k : ℕ) ≤ (m : ℕ) ∧ (mod m k : ℕ) ≤ (k : ℕ)
[GOAL]
m k : ℕ+
⊢ ↑(mod m k) ≤ ↑m ∧ ↑(mod m k) ≤ ↑k
[PROOFSTEP]
rw [mod_coe]
[GOAL]
m k : ℕ+
⊢ (if ↑m % ↑k = 0 then ↑k else ↑m % ↑k) ≤ ↑m ∧ (if ↑m % ↑k = 0 then ↑k else ↑m % ↑k) ≤ ↑k
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
m k : ℕ+
h : ↑m % ↑k = 0
⊢ ↑k ≤ ↑m ∧ ↑k ≤ ↑k
[PROOFSTEP]
have hm : (m : ℕ) > 0 := m.pos
[GOAL]
case pos
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑m > 0
⊢ ↑k ≤ ↑m ∧ ↑k ≤ ↑k
[PROOFSTEP]
rw [← Nat.mod_add_div (m : ℕ) (k : ℕ), h, zero_add] at hm ⊢
[GOAL]
case pos
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑k * (↑m / ↑k) > 0
⊢ ↑k ≤ ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k
[PROOFSTEP]
by_cases h₁ : (m : ℕ) / (k : ℕ) = 0
[GOAL]
case pos
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑k * (↑m / ↑k) > 0
h₁ : ↑m / ↑k = 0
⊢ ↑k ≤ ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k
[PROOFSTEP]
rw [h₁, mul_zero] at hm 
[GOAL]
case pos
m k : ℕ+
h : ↑m % ↑k = 0
hm : 0 > 0
h₁ : ↑m / ↑k = 0
⊢ ↑k ≤ ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k
[PROOFSTEP]
exact (lt_irrefl _ hm).elim
[GOAL]
case neg
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑k * (↑m / ↑k) > 0
h₁ : ¬↑m / ↑k = 0
⊢ ↑k ≤ ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k
[PROOFSTEP]
let h₂ : (k : ℕ) * 1 ≤ k * (m / k) :=
  -- Porting note : Specified type of `h₂` explicitly because `rw` could not unify
          -- `succ 0` with `1`.Nat.mul_le_mul_left (k : ℕ) (Nat.succ_le_of_lt (Nat.pos_of_ne_zero h₁))
[GOAL]
case neg
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑k * (↑m / ↑k) > 0
h₁ : ¬↑m / ↑k = 0
h₂ : ↑k * 1 ≤ ↑k * (↑m / ↑k) := Nat.mul_le_mul_left (↑k) (succ_le_of_lt (Nat.pos_of_ne_zero h₁))
⊢ ↑k ≤ ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k
[PROOFSTEP]
rw [mul_one] at h₂ 
[GOAL]
case neg
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑k * (↑m / ↑k) > 0
h₁ : ¬↑m / ↑k = 0
h₂ : ↑k ≤ ↑k * (↑m / ↑k)
⊢ ↑k ≤ ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k
[PROOFSTEP]
exact ⟨h₂, le_refl (k : ℕ)⟩
[GOAL]
case neg
m k : ℕ+
h : ¬↑m % ↑k = 0
⊢ ↑m % ↑k ≤ ↑m ∧ ↑m % ↑k ≤ ↑k
[PROOFSTEP]
exact ⟨Nat.mod_le (m : ℕ) (k : ℕ), (Nat.mod_lt (m : ℕ) k.pos).le⟩
[GOAL]
k m : ℕ+
⊢ k ∣ m ↔ ↑k ∣ ↑m
[PROOFSTEP]
constructor
[GOAL]
case mp
k m : ℕ+
⊢ k ∣ m → ↑k ∣ ↑m
[PROOFSTEP]
intro h
[GOAL]
case mpr
k m : ℕ+
⊢ ↑k ∣ ↑m → k ∣ m
[PROOFSTEP]
intro h
[GOAL]
case mp
k m : ℕ+
h : k ∣ m
⊢ ↑k ∣ ↑m
[PROOFSTEP]
rcases h with ⟨_, rfl⟩
[GOAL]
case mp.intro
k w✝ : ℕ+
⊢ ↑k ∣ ↑(k * w✝)
[PROOFSTEP]
apply dvd_mul_right
[GOAL]
case mpr
k m : ℕ+
h : ↑k ∣ ↑m
⊢ k ∣ m
[PROOFSTEP]
rcases h with ⟨a, h⟩
[GOAL]
case mpr.intro
k m : ℕ+
a : ℕ
h : ↑m = ↑k * a
⊢ k ∣ m
[PROOFSTEP]
cases a with
| zero =>
  contrapose h
  apply ne_zero
| succ n =>
  use⟨n.succ, n.succ_pos⟩
  rw [← coe_inj, h, mul_coe, mk_coe]
[GOAL]
case mpr.intro
k m : ℕ+
a : ℕ
h : ↑m = ↑k * a
⊢ k ∣ m
[PROOFSTEP]
cases a with
| zero =>
  contrapose h
  apply ne_zero
| succ n =>
  use⟨n.succ, n.succ_pos⟩
  rw [← coe_inj, h, mul_coe, mk_coe]
[GOAL]
case mpr.intro.zero
k m : ℕ+
h : ↑m = ↑k * zero
⊢ k ∣ m
[PROOFSTEP]

| zero =>
  contrapose h
  apply ne_zero
[GOAL]
case mpr.intro.zero
k m : ℕ+
h : ↑m = ↑k * zero
⊢ k ∣ m
[PROOFSTEP]
contrapose h
[GOAL]
case mpr.intro.zero
k m : ℕ+
h : ¬k ∣ m
⊢ ¬↑m = ↑k * zero
[PROOFSTEP]
apply ne_zero
[GOAL]
case mpr.intro.succ
k m : ℕ+
n : ℕ
h : ↑m = ↑k * succ n
⊢ k ∣ m
[PROOFSTEP]

| succ n =>
  use⟨n.succ, n.succ_pos⟩
  rw [← coe_inj, h, mul_coe, mk_coe]
[GOAL]
case mpr.intro.succ
k m : ℕ+
n : ℕ
h : ↑m = ↑k * succ n
⊢ k ∣ m
[PROOFSTEP]
use⟨n.succ, n.succ_pos⟩
[GOAL]
case h
k m : ℕ+
n : ℕ
h : ↑m = ↑k * succ n
⊢ m = k * { val := succ n, property := (_ : 0 < succ n) }
[PROOFSTEP]
rw [← coe_inj, h, mul_coe, mk_coe]
[GOAL]
k m : ℕ+
⊢ k ∣ m ↔ mod m k = k
[PROOFSTEP]
rw [dvd_iff]
[GOAL]
k m : ℕ+
⊢ ↑k ∣ ↑m ↔ mod m k = k
[PROOFSTEP]
rw [Nat.dvd_iff_mod_eq_zero]
[GOAL]
k m : ℕ+
⊢ ↑m % ↑k = 0 ↔ mod m k = k
[PROOFSTEP]
constructor
[GOAL]
case mp
k m : ℕ+
⊢ ↑m % ↑k = 0 → mod m k = k
[PROOFSTEP]
intro h
[GOAL]
case mp
k m : ℕ+
h : ↑m % ↑k = 0
⊢ mod m k = k
[PROOFSTEP]
apply PNat.eq
[GOAL]
case mp.a
k m : ℕ+
h : ↑m % ↑k = 0
⊢ ↑(mod m k) = ↑k
[PROOFSTEP]
rw [mod_coe, if_pos h]
[GOAL]
case mpr
k m : ℕ+
⊢ mod m k = k → ↑m % ↑k = 0
[PROOFSTEP]
intro h
[GOAL]
case mpr
k m : ℕ+
h : mod m k = k
⊢ ↑m % ↑k = 0
[PROOFSTEP]
by_cases h' : (m : ℕ) % (k : ℕ) = 0
[GOAL]
case pos
k m : ℕ+
h : mod m k = k
h' : ↑m % ↑k = 0
⊢ ↑m % ↑k = 0
[PROOFSTEP]
exact h'
[GOAL]
case neg
k m : ℕ+
h : mod m k = k
h' : ¬↑m % ↑k = 0
⊢ ↑m % ↑k = 0
[PROOFSTEP]
replace h : (mod m k : ℕ) = (k : ℕ) := congr_arg _ h
[GOAL]
case neg
k m : ℕ+
h' : ¬↑m % ↑k = 0
h : ↑(mod m k) = ↑k
⊢ ↑m % ↑k = 0
[PROOFSTEP]
rw [mod_coe, if_neg h'] at h 
[GOAL]
case neg
k m : ℕ+
h' : ¬↑m % ↑k = 0
h : ↑m % ↑k = ↑k
⊢ ↑m % ↑k = 0
[PROOFSTEP]
exact ((Nat.mod_lt (m : ℕ) k.pos).ne h).elim
[GOAL]
m n : ℕ+
⊢ m ∣ n → m ≤ n
[PROOFSTEP]
rw [dvd_iff']
[GOAL]
m n : ℕ+
⊢ mod n m = m → m ≤ n
[PROOFSTEP]
intro h
[GOAL]
m n : ℕ+
h : mod n m = m
⊢ m ≤ n
[PROOFSTEP]
rw [← h]
[GOAL]
m n : ℕ+
h : mod n m = m
⊢ mod n m ≤ n
[PROOFSTEP]
apply (mod_le n m).left
[GOAL]
m k : ℕ+
h : k ∣ m
⊢ k * divExact m k = m
[PROOFSTEP]
apply PNat.eq
[GOAL]
case a
m k : ℕ+
h : k ∣ m
⊢ ↑(k * divExact m k) = ↑m
[PROOFSTEP]
rw [mul_coe]
[GOAL]
case a
m k : ℕ+
h : k ∣ m
⊢ ↑k * ↑(divExact m k) = ↑m
[PROOFSTEP]
change (k : ℕ) * (div m k).succ = m
[GOAL]
case a
m k : ℕ+
h : k ∣ m
⊢ ↑k * succ (div m k) = ↑m
[PROOFSTEP]
rw [← div_add_mod m k, dvd_iff'.mp h, Nat.mul_succ]
[GOAL]
n : ℕ+
a : ℕ
h : a ∣ ↑n
⊢ 0 < a
[PROOFSTEP]
apply pos_iff_ne_zero.2
[GOAL]
n : ℕ+
a : ℕ
h : a ∣ ↑n
⊢ a ≠ 0
[PROOFSTEP]
intro hzero
[GOAL]
n : ℕ+
a : ℕ
h : a ∣ ↑n
hzero : a = 0
⊢ False
[PROOFSTEP]
rw [hzero] at h 
[GOAL]
n : ℕ+
a : ℕ
h : 0 ∣ ↑n
hzero : a = 0
⊢ False
[PROOFSTEP]
exact PNat.ne_zero n (eq_zero_of_zero_dvd h)
