feat(algebra/order/floor): some nat.ceil lemmas (#16987)

mostly for feature completeness with the int version

`nat.ceil_coe` is renamed to `nat.ceil_nat_cast` to match the int version

src/algebra/order/floor.lean

@@ -185,16 +185,29 @@ lemma gc_ceil_coe : galois_connection (ceil : α → ℕ) coe := floor_semiring.
 
 lemma lt_ceil : n < ⌈a⌉₊ ↔ (n : α) < a := lt_iff_lt_of_le_iff_le ceil_le
 
+@[simp] lemma add_one_le_ceil_iff : n + 1 ≤ ⌈a⌉₊ ↔ (n : α) < a :=
+by rw [← nat.lt_ceil, nat.add_one_le_iff]
+
+@[simp] lemma one_le_ceil_iff : 1 ≤ ⌈a⌉₊ ↔ 0 < a :=
+by rw [← zero_add 1, nat.add_one_le_ceil_iff, nat.cast_zero]
+
+lemma ceil_le_floor_add_one (a : α) : ⌈a⌉₊ ≤ ⌊a⌋₊ + 1 :=
+by { rw [ceil_le, nat.cast_add, nat.cast_one], exact (lt_floor_add_one a).le }
+
 lemma le_ceil (a : α) : a ≤ ⌈a⌉₊ := ceil_le.1 le_rfl
 
-lemma ceil_mono : monotone (ceil : α → ℕ) := gc_ceil_coe.monotone_l
+@[simp] lemma ceil_int_cast {α : Type*} [linear_ordered_ring α]
+  [floor_semiring α] (z : ℤ) : ⌈(z : α)⌉₊ = z.to_nat :=
+eq_of_forall_ge_iff $ λ a, by { simp, norm_cast }
+
+@[simp] lemma ceil_nat_cast (n : ℕ) : ⌈(n : α)⌉₊ = n :=
+eq_of_forall_ge_iff $ λ a, by rw [ceil_le, cast_le]
 
-@[simp] lemma ceil_coe (n : ℕ) : ⌈(n : α)⌉₊ = n :=
-eq_of_forall_ge_iff $ λ a, ceil_le.trans nat.cast_le
+lemma ceil_mono : monotone (ceil : α → ℕ) := gc_ceil_coe.monotone_l
 
-@[simp] lemma ceil_zero : ⌈(0 : α)⌉₊ = 0 := by rw [← nat.cast_zero, ceil_coe]
+@[simp] lemma ceil_zero : ⌈(0 : α)⌉₊ = 0 := by rw [← nat.cast_zero, ceil_nat_cast]
 
-@[simp] lemma ceil_one : ⌈(1 : α)⌉₊ = 1 := by rw [←nat.cast_one, ceil_coe]
+@[simp] lemma ceil_one : ⌈(1 : α)⌉₊ = 1 := by rw [←nat.cast_one, ceil_nat_cast]
 
 @[simp] lemma ceil_eq_zero : ⌈a⌉₊ = 0 ↔ a ≤ 0 := by rw [← le_zero_iff, ceil_le, nat.cast_zero]
 

src/data/int/log.lean

@@ -136,7 +136,7 @@ begin
       zpow_coe_nat, ←nat.cast_pow, nat.floor_coe, nat.log_pow hb],
     exact_mod_cast hb.le, },
   { rw [log_of_right_le_one _ (zpow_le_one_of_nonpos _ $ neg_nonpos.mpr (int.coe_nat_nonneg _)),
-      zpow_neg, inv_inv, zpow_coe_nat, ←nat.cast_pow, nat.ceil_coe, nat.clog_pow _ _ hb],
+      zpow_neg, inv_inv, zpow_coe_nat, ←nat.cast_pow, nat.ceil_nat_cast, nat.clog_pow _ _ hb],
     exact_mod_cast hb.le, },
 end