no goals
d✝ : ℤ
c d b : ℕ
⊢ Nonnegg c d (-↑0) ↑b → SqLe 0 d b c
simp [SqLe, Nat.zero_le]
d✝ : ℤ
c d a b : ℕ
⊢ Nonnegg c d (Int.negSucc a) ↑b ↔ SqLe (a + 1) d b c
d✝ : ℤ
c d a b : ℕ
⊢ Nonnegg c d (-↑(a + 1)) ↑b ↔ SqLe (a + 1) d b c
rw [← Int.negSucc_coe]
no goals
d✝ : ℤ
c d a b : ℕ
⊢ Nonnegg c d (Int.negSucc a) ↑b ↔ SqLe (a + 1) d b c
rfl