chore(algebra/floor): add a trivial lemma (#9098)

* add `nat_ceil_eq_zero`;
* add `@[simp]` to `nat_ceil_le`.

Author: urkud

src/algebra/floor.lean

@@ -359,7 +359,7 @@ def nat_ceil (a : α) : ℕ := int.to_nat ⌈a⌉
 
 notation `⌈` x `⌉₊` := nat_ceil x
 
-theorem nat_ceil_le : ⌈a⌉₊ ≤ n ↔ a ≤ n :=
+@[simp] theorem nat_ceil_le : ⌈a⌉₊ ≤ n ↔ a ≤ n :=
 by rw [nat_ceil, int.to_nat_le, ceil_le]; refl
 
 theorem lt_nat_ceil : n < ⌈a⌉₊ ↔ (n : α) < a :=
@@ -375,6 +375,9 @@ show (⌈((n : ℤ) : α)⌉).to_nat = n, by rw [ceil_coe]; refl
 
 @[simp] theorem nat_ceil_zero : ⌈(0 : α)⌉₊ = 0 := nat_ceil_coe 0
 
+@[simp] theorem nat_ceil_eq_zero : ⌈a⌉₊ = 0 ↔ a ≤ 0 :=
+by simp [← nonpos_iff_eq_zero]
+
 theorem nat_ceil_add_nat {a : α} (a_nonneg : 0 ≤ a) (n : ℕ) : ⌈a + n⌉₊ = ⌈a⌉₊ + n :=
 begin
   change int.to_nat (⌈a + (n:ℤ)⌉) = int.to_nat ⌈a⌉ + n,