[Merged by Bors] - feat(data/nat/basic): Add two lemmas two nat/basic which are necessary for the count PR

src/data/nat/basic.lean

@@ -108,6 +108,9 @@ instance nat.subtype.semilattice_sup_bot (s : set ℕ) [decidable_pred (∈ s)]
   ..subtype.linear_order s,
   ..lattice_of_linear_order }
 
+lemma nat.subtype.coe_bot {s : set ℕ} [decidable_pred (∈ s)]
+  [h : nonempty s] : ((⊥ : s) : ℕ) = nat.find (nonempty_subtype.1 h) := rfl
+
 theorem nat.nsmul_eq_mul (m n : ℕ) : m • n = m * n :=
 rfl
 
@@ -510,6 +513,9 @@ begin
     exact nat.le_of_pred_lt h', },
 end
 
+/-- A version of `nat.sub_succ` in the form `_ - 1` instead of `nat.pred _`. -/
+lemma sub_succ' (a b : ℕ) : a - b.succ = a - b - 1 := rfl
+
 /-! ### `mul` -/
 
 lemma succ_mul_pos (m : ℕ) (hn : 0 < n) : 0 < (succ m) * n :=