[GOAL]
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
⊢ 0 ≤ toNat (a % ↑n) ∧ toNat (a % ↑n) < n ∧ a ≡ ↑(toNat (a % ↑n)) [ZMOD ↑n]
[PROOFSTEP]
have := ofNat_pos.2 <| Nat.le_of_ble_eq_true hn
[GOAL]
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : 0 < ↑n
⊢ 0 ≤ toNat (a % ↑n) ∧ toNat (a % ↑n) < n ∧ a ≡ ↑(toNat (a % ↑n)) [ZMOD ↑n]
[PROOFSTEP]
have nonneg := emod_nonneg a <| Int.ne_of_gt this
[GOAL]
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : 0 < ↑n
nonneg : 0 ≤ a % ↑n
⊢ 0 ≤ toNat (a % ↑n) ∧ toNat (a % ↑n) < n ∧ a ≡ ↑(toNat (a % ↑n)) [ZMOD ↑n]
[PROOFSTEP]
refine ⟨Nat.zero_le _, ?_, ?_⟩
[GOAL]
case refine_1
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : 0 < ↑n
nonneg : 0 ≤ a % ↑n
⊢ toNat (a % ↑n) < n
[PROOFSTEP]
rw [Int.toNat_lt nonneg]
[GOAL]
case refine_1
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : 0 < ↑n
nonneg : 0 ≤ a % ↑n
⊢ a % ↑n < ↑n
[PROOFSTEP]
exact Int.emod_lt_of_pos _ this
[GOAL]
case refine_2
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : 0 < ↑n
nonneg : 0 ≤ a % ↑n
⊢ a ≡ ↑(toNat (a % ↑n)) [ZMOD ↑n]
[PROOFSTEP]
rw [Int.ModEq, Int.toNat_of_nonneg nonneg, emod_emod]
