feat(data/nat/choose/basic): add some inequalities showing that choos…

…e is monotonic in the first argument (#10102)

From flt-regular

src/data/nat/choose/basic.lean

@@ -267,4 +267,21 @@ begin
     apply zero_le }
 end
 
+/-! #### Inequalities about increasing the first argument -/
+
+lemma choose_le_succ (a c : ℕ) : choose a c ≤ choose a.succ c :=
+by cases c; simp [nat.choose_succ_succ]
+
+lemma choose_le_add (a b c : ℕ) : choose a c ≤ choose (a + b) c :=
+begin
+  induction b with b_n b_ih,
+  { simp, },
+  exact le_trans b_ih (choose_le_succ (a + b_n) c),
+end
+
+lemma choose_le_choose {a b : ℕ} (c : ℕ) (h : a ≤ b) : choose a c ≤ choose b c :=
+(add_tsub_cancel_of_le h) ▸ choose_le_add a (b - a) c
+
+lemma choose_mono (b : ℕ) : monotone (λ a, choose a b) := λ _ _, choose_le_choose b
+
 end nat