# Zulip Chat Archive

## Stream: new members

### Topic: Tidying up a proof

#### Bhavik Mehta (Nov 19 2019 at 10:53):

Hi all, I've written a proof for a (seemingly) simple statement, but I feel like it could be simplified a lot. Any comments or suggestions appreciated!

lemma sub_sub_assoc {r k n : ℕ} (h1 : k ≤ r) (h2 : r ≤ n) : n - r + k = n - (r - k) := by omega lemma fact_pred {r : ℕ} (h : r > 0) : nat.fact r = r * nat.fact (r-1) := calc nat.fact r = nat.fact (nat.succ (r-1)) : by rw [← nat.pred_eq_sub_one, nat.succ_pred_eq_of_pos h] ... = nat.succ (r-1) * nat.fact (r-1) : nat.fact_succ _ ... = r * nat.fact (r-1) : by rw [← nat.pred_eq_sub_one, nat.succ_pred_eq_of_pos h] lemma choose_lemma {n r : ℕ} (hr1 : 1 ≤ r) (hr2 : r ≤ n) : (n - r + 1) * nat.choose n (r-1) = nat.choose n r * r := begin have: r - 1 ≤ n := le_trans (nat.pred_le r) ‹r ≤ n›, apply nat.eq_of_mul_eq_mul_right (mul_pos (nat.fact_pos (r-1)) (nat.fact_pos (n-r))), by calc (n - r + 1) * nat.choose n (r - 1) * (nat.fact (r - 1) * nat.fact (n - r)) = nat.choose n (r-1) * nat.fact (r-1) * ((n - r + 1) * nat.fact (n - r)) : by rw [mul_assoc, mul_comm]; simp only [mul_assoc]; rw mul_comm _ (n-r+1) ... = nat.choose n (r-1) * nat.fact (r-1) * nat.fact (n - r + 1) : by rw ← nat.fact_succ ... = nat.choose n (r-1) * nat.fact (r-1) * nat.fact (n - (r - 1)) : by rw sub_sub_assoc hr1 hr2 ... = nat.fact n : by rw nat.choose_mul_fact_mul_fact ‹r - 1 ≤ n› ... = nat.choose n r * nat.fact r * nat.fact (n - r) : by rw ← nat.choose_mul_fact_mul_fact ‹r ≤ n› ... = nat.choose n r * (r * nat.fact (r - 1)) * nat.fact (n - r) : by rw fact_pred ‹r ≥ 1› ... = nat.choose n r * r * (nat.fact (r - 1) * nat.fact (n - r)) : by simp only [mul_assoc], end theorem main_lemma {A B n r : ℕ} (hr1 : 1 ≤ r) (hr2 : r ≤ n) : A * r ≤ B * (n - r + 1) → (A : ℚ) / (nat.choose n r) ≤ B / nat.choose n (r-1) := begin intro k, have: r - 1 ≤ n := le_trans (nat.pred_le r) ‹r ≤ n›, have: 0 < nat.choose n (r-1) := nat.choose_pos ‹r - 1 ≤ n›, have: 0 < nat.choose n r := nat.choose_pos ‹r ≤ n›, rw [div_le_iff', mul_comm, div_mul_eq_mul_div, le_div_iff]; norm_cast, rotate, assumption, assumption, apply le_of_mul_le_mul_right _, exact hr1, by calc A * nat.choose n (r - 1) * r = A * r * nat.choose n (r-1) : by rw [nat.mul_assoc, nat.mul_comm _ r, ← nat.mul_assoc] ... ≤ B * (n - r + 1) * nat.choose n (r-1) : by apply nat.mul_le_mul_right _ k ... = B * nat.choose n r * r : by rw [mul_assoc, mul_assoc, choose_lemma hr1 hr2] end

I don't have need for any of the internal lemmas so feel free to rearrange/remove them, as long as `main_lemma`

looks pretty much the same.

Thanks!

#### Edward Ayers (Nov 19 2019 at 11:16):

You can use `ac_refl`

on the first and last steps of the calc in `choose_lemma`

#### Bhavik Mehta (Nov 19 2019 at 11:18):

Ooooh nice thanks

#### Mario Carneiro (Nov 19 2019 at 11:29):

I managed the following alternate proof:

theorem div_le_div_iff {α} [linear_ordered_field α] {a b c d : α} (hc : 0 < c) (hd : 0 < d) : a / c ≤ b / d ↔ a * d ≤ b * c := by rw [le_div_iff hd, div_mul_eq_mul_div, div_le_iff hc] lemma nat.choose_succ_right_eq (n k) (h : k + 1 ≤ n) : nat.choose n (k + 1) * (k + 1) = nat.choose n k * (n - k) := begin have e : n - (k + 1) + 1 = n - k, { rw [← nat.sub_add_comm h, nat.add_sub_add_right] }, have := nat.choose_mul_fact_mul_fact (le_of_lt h), rw [← nat.choose_mul_fact_mul_fact h, nat.fact_succ, ← e, nat.fact_succ, nat.succ_eq_add_one, e, nat.succ_eq_add_one, ← mul_assoc, nat.mul_right_inj (nat.fact_pos _), ← mul_assoc, mul_right_comm, nat.mul_right_inj (nat.fact_pos _)] at this, rw this end theorem main_lemma {A B n r : ℕ} (hr1 : 1 ≤ r) (hr2 : r ≤ n) (h : A * r ≤ B * (n - r + 1)) : (A : ℚ) / (nat.choose n r) ≤ B / nat.choose n (r-1) := begin rw [div_le_div_iff]; norm_cast, { cases r, cases hr1, rw ← mul_le_mul_right (nat.succ_pos r), rw nat.succ_eq_add_one at *, rw [← nat.sub_add_comm hr2, nat.add_sub_add_right] at h, rw [nat.add_sub_cancel, mul_assoc B, nat.choose_succ_right_eq _ _ hr2, mul_right_comm, ← mul_assoc, mul_right_comm B], exact nat.mul_le_mul_right _ h }, { exact nat.choose_pos hr2 }, { exact nat.choose_pos (le_trans (nat.sub_le _ _) hr2) } end

#### Kevin Buzzard (Nov 19 2019 at 14:06):

`example (n : ℕ) : n > 0 → ¬ (n = 0) := by ??`

Which tactic finishes this? Or is it a function? I couldn't find it :-/

#### Kevin Buzzard (Nov 19 2019 at 14:06):

`example (n : ℕ) : n > 0 → ¬ (n = 0) := by intros; linarith`

:D

#### Mario Carneiro (Nov 19 2019 at 14:06):

`ne_of_lt`

or `ne_of_gt`

#### Kevin Buzzard (Nov 19 2019 at 14:07):

aah I was foolishly looking for `ne_zero_of_pos`

#### Kevin Buzzard (Nov 19 2019 at 14:43):

I tried multiplying everything out but it was horrible :-(

import data.rat tactic.linarith open nat -- this should be in mathlib, right? theorem div_le_div_iff {α} [linear_ordered_field α] {a b c d : α} (hc : 0 < c) (hd : 0 < d) : a / c ≤ b / d ↔ a * d ≤ b * c := by rw [le_div_iff hd, div_mul_eq_mul_div, div_le_iff hc] -- Should this be in data.rat? It doesn't easily follow from nat.choose_eq_fact_div_fact def rat.choose_eq_fact_div_fact (n k : ℕ) (h : k ≤ n) : (choose n k : ℚ) = fact n / (fact k * fact (n - k)) := eq_div_of_mul_eq _ _ (mul_ne_zero (ne_of_gt $ by simp [fact_pos]) (ne_of_gt $ by simp [fact_pos])) $ begin norm_cast, rw ←mul_assoc, exact choose_mul_fact_mul_fact h end -- s = r - 1 theorem main_lemma {A B n s : ℕ} (hr2 : s + 1 ≤ n) (h : A * (s + 1) ≤ B * (n - s)) : (A : ℚ) / (nat.choose n (s + 1)) ≤ B / nat.choose n s := begin rw [rat.choose_eq_fact_div_fact, rat.choose_eq_fact_div_fact, div_div_eq_mul_div, div_div_eq_mul_div], apply div_le_div_of_le_of_pos, norm_cast, rw [←@nat.sub_add_cancel (n - s) 1, fact_succ, fact_succ, ←succ_sub, succ_sub_one, nat.sub_sub], rw [show A * (succ s * fact s * fact (n - (s + 1))) = A * (s + 1) * (fact s * fact (n - (s + 1))), by ring], rw [show B * (fact s * ((n - s) * fact (n - (s + 1)))) = B * (n - s) * (fact s * fact (n - (s + 1))), by ac_refl], refine mul_le_mul_right _ h, repeat {linarith}, exact nat.le_sub_left_of_add_le hr2, exact nat.le_sub_left_of_add_le hr2, norm_cast, apply fact_pos, end

#### Kevin Buzzard (Nov 19 2019 at 14:45):

This surprised me along the way:

example (B s n : ℕ) : B * (fact s * ((n - s) * fact (n - s - 1))) = B * (n - s) * (fact s * fact (n - s - 1)) := begin -- ac_refl, -- closes goal ring, -- does not close goal sorry end

@Mario Carneiro would you have expected `ring`

to work there?

#### Mario Carneiro (Nov 19 2019 at 14:46):

yes

#### Mario Carneiro (Nov 19 2019 at 14:47):

Whenever `ring`

fails, try `ring1`

, which reports a useful error instead of doing a fall back thing

#### Kevin Buzzard (Nov 19 2019 at 14:48):

example (f1 n s: ℕ) : f1 * (n - s) = (n - s) * f1 := by ring -- fails

#### Kevin Buzzard (Nov 19 2019 at 14:49):

app_builder_exception, more information can be obtained using command `set_option trace.app_builder true` state: f1 n s : ℕ ⊢ f1 * (n - s) = (n - s) * f1

is the output from `ring1`

#### Kevin Buzzard (Nov 19 2019 at 14:49):

[app_builder] failed to create an 'has_neg.neg'-application, there are missing implicit arguments

#### Mario Carneiro (Nov 19 2019 at 14:50):

it thinks the subtraction is ring subtraction, and builds a bad term

#### Kevin Buzzard (Nov 19 2019 at 14:50):

I can generalize my way out of this I guess

#### Kevin Buzzard (Nov 19 2019 at 14:50):

"you don't know this, but n-s is an atom"

#### Kevin Buzzard (Nov 19 2019 at 14:51):

Why does multiplying it all out hurt so much? That's an algorithmic way to solve this problem [I'm now talking about the original q]

#### Kevin Buzzard (Nov 19 2019 at 14:54):

What would the Isabelle proof of this triviality look like? @Sebastien Gouezel do you know?

#### Mario Carneiro (Nov 19 2019 at 14:55):

what do you want to be less painful?

#### Mario Carneiro (Nov 19 2019 at 14:55):

there are several interacting things here

#### Mario Carneiro (Nov 19 2019 at 14:56):

I think the real thing is that the lemma I called `nat.choose_succ_right_eq`

was missing

#### Mario Carneiro (Nov 19 2019 at 14:56):

one of the basic facts about choose is how it changes when you move by one in any direction

#### Mario Carneiro (Nov 19 2019 at 14:57):

`div_le_div_iff`

missing is even more scandalous. I would have expected that in core

#### Mario Carneiro (Nov 19 2019 at 14:58):

-- Should this be in data.rat? It doesn't easily follow from nat.choose_eq_fact_div_fact def rat.choose_eq_fact_div_fact (n k : ℕ) (h : k ≤ n) : (choose n k : ℚ) = fact n / (fact k * fact (n - k)) :=

It does easily follow from `choose_mul_fact_mul_fact`

though

#### Sebastien Gouezel (Nov 19 2019 at 15:13):

What would the Isabelle proof of this triviality look like? Sebastien Gouezel do you know?

Isabelle automation is order of magnitudes better. So, anything will work. I just tried it:

lemma for_kevin: fixes f1 n s::nat shows "f1 * (n-s) = (n-s) * f1" by simp

You can replace `by simp`

with `by auto`

, or `by algebra`

, or `by fastforce`

, or `by force`

. In fact, I just typed `try0`

and Isabelle suggested all these solutions right away.

#### Mario Carneiro (Nov 19 2019 at 15:14):

I think he's talking about the choose proof

#### Sebastien Gouezel (Nov 19 2019 at 15:15):

Which statement?

#### Mario Carneiro (Nov 19 2019 at 15:16):

Probably `main_lemma`

?

#### Kevin Buzzard (Nov 19 2019 at 15:16):

theorem main_lemma {A B n r : ℕ} (hr1 : 1 ≤ r) (hr2 : r ≤ n) : A * r ≤ B * (n - r + 1) → (A : ℚ) / (nat.choose n r) ≤ B / nat.choose n (r-1) :=

#### Kevin Buzzard (Nov 19 2019 at 15:17):

I really want this to be easy

#### Mario Carneiro (Nov 19 2019 at 15:17):

I get the sense that kevin's proof is a tactic bash

#### Kevin Buzzard (Nov 19 2019 at 15:17):

My proof is "LOOK. $\binom{n}{r}=\frac{n!}{r!(n-r)!}$ AND THE REST IS TRIVIAL"

#### Mario Carneiro (Nov 19 2019 at 15:18):

This sort of proof feels easier in metamath to me

#### Kevin Buzzard (Nov 19 2019 at 15:18):

(assuming `fact_succ`

)

#### Mario Carneiro (Nov 19 2019 at 15:18):

all this business with saturating subtraction isn't a problem

#### Mario Carneiro (Nov 19 2019 at 15:20):

It might help if `nat.choose`

was defined over integers

#### Kevin Buzzard (Nov 19 2019 at 15:26):

-- Should this be in data.rat? It doesn't easily follow from nat.choose_eq_fact_div_fact def rat.choose_eq_fact_div_fact (n k : ℕ) (h : k ≤ n) : (choose n k : ℚ) = fact n / (fact k * fact (n - k)) :=It does easily follow from

`choose_mul_fact_mul_fact`

though

My proof was an attempt to show this and it was still pretty horrible. What am I missing?

#### Kevin Buzzard (Nov 19 2019 at 15:27):

import data.rat tactic.linarith open nat -- this should be in mathlib, right? theorem div_le_div_iff {α} [linear_ordered_field α] {a b c d : α} (hc : 0 < c) (hd : 0 < d) : a / c ≤ b / d ↔ a * d ≤ b * c := by rw [le_div_iff hd, div_mul_eq_mul_div, div_le_iff hc] -- Should this be in data.rat? It doesn't easily follow from nat.choose_eq_fact_div_fact def rat.choose_eq_fact_div_fact (n k : ℕ) (h : k ≤ n) : (choose n k : ℚ) = fact n / (fact k * fact (n - k)) := eq_div_of_mul_eq _ _ (mul_ne_zero (ne_of_gt $ by simp [fact_pos]) (ne_of_gt $ by simp [fact_pos])) $ begin norm_cast, rw ←mul_assoc, exact choose_mul_fact_mul_fact h end -- r = s + 1 -- n = t + 1 + s theorem main_lemma {A B s t : ℕ} (h : A * (s + 1) ≤ B * (t + 1)) : (A : ℚ) / (nat.choose (t + 1 + s) (s + 1)) ≤ B / nat.choose (t + 1 + s) s := begin rw [rat.choose_eq_fact_div_fact, rat.choose_eq_fact_div_fact, div_div_eq_mul_div, div_div_eq_mul_div], apply div_le_div_of_le_of_pos, norm_cast, rw [nat.add_sub_cancel, add_right_comm, add_assoc, nat.add_sub_cancel, fact_succ, fact_succ], convert nat.mul_le_mul_right (fact s * fact t) h using 1, repeat {linarith}, repeat {rw succ_eq_add_one; ring}, norm_cast, apply fact_pos, end

Using less painful variables s and t I can get it down to this.

#### Kevin Buzzard (Nov 19 2019 at 15:30):

But if Isabelle can just blast through it then this will give me a better understanding of what we are missing in Lean. This proof should be trivial given some hints -- shouldn't it? `by schoolkid using [choose_mul_fact_mul_fact, fact_pos, fact_succ]`

#### Mario Carneiro (Nov 19 2019 at 15:30):

I think you got it down pretty well.

theorem rat.choose_eq_fact_div_fact (n k : ℕ) (h : k ≤ n) : (choose n k : ℚ) = fact n / (fact k * fact (n - k)) := by rw eq_div_iff_mul_eq; norm_cast; [ rw [← mul_assoc, choose_mul_fact_mul_fact h], exact ne_of_gt (mul_pos (fact_pos _) (fact_pos _))]

#### Mario Carneiro (Nov 19 2019 at 15:31):

If you have a sledgehammer then you can make it through this, I think

#### Kevin Buzzard (Nov 19 2019 at 15:31):

because all schoolkids know `div_div_eq_mul_div, div_le_div_of_le_of_pos, div_div_eq_mul_div, nat.add_sub_cancel`

etc

#### Mario Carneiro (Nov 19 2019 at 15:32):

they also know a number of false variations on those :P

#### Kevin Buzzard (Nov 19 2019 at 15:32):

Yeah, it's a pretty powerful tactic. You can prove `false`

with it if you're not careful

#### Kevin Buzzard (Nov 19 2019 at 15:33):

I started my lectures this year with a proof that all triangles were equilateral and it was only once I'd finished that people started complaining; I made the error about 10 lines before that.

#### Kevin Buzzard (Nov 19 2019 at 15:33):

They were happy with the method but uncomfortable with the conclusion

#### Sebastien Gouezel (Nov 19 2019 at 15:43):

Here is an Isabelle proof:

lemma for_kevin2: fixes A B n r::nat assumes "1 ≤ r" "r ≤ n" "A * r ≤ B * (n-r+1)" shows "A / (binomial n r) ≤ B / (binomial n (r-1))" proof - have I: "binomial n r = (fact n)/(fact r * fact (n-r))" using assms(2) binomial_fact by blast have J : "binomial n (r-1) = (fact n)/(fact (r-1) * fact (n+1-r))" using assms(1) assms(2) binomial_fact[of "r-1" n] by force have K : "fact r = of_nat r * fact (r-1)" using fact_reduce[of r] assms(1) by auto have L : "fact (n+1-r) = of_nat (n+1-r) * fact (n-r)" using fact_reduce[of "n+1-r"] assms by auto show ?thesis unfolding I J K L apply (auto simp add: divide_simps) by (metis Suc_diff_le Suc_eq_plus1_left add.commute assms(2) assms(3) of_nat_mono of_nat_mult) qed

I still had to help it a little bit giving the auxiliary statements `I`

, `J`

, `K`

, `L`

. The last line is needed since my assumption is formulated for integer numbers but the conclusion needs it over rationals (in fact here over the reals, as Isabelle coerced everything to reals when I wrote the division). The point is I didn't write this line, it was found by sledgehammer.

#### Sebastien Gouezel (Nov 19 2019 at 15:46):

I should tell you what `binomial_fact`

and `fact_reduce`

are, by the way. They are preexisting facts in the library, as follows.

lemma fact_reduce: "n > 0 ⟹ fact n = of_nat n * fact (n - 1)" by (cases n) auto lemma binomial_fact: assumes kn: "k ≤ n" shows "(of_nat (n choose k) :: 'a::field_char_0) = fact n / (fact k * fact (n - k))"

#### Kevin Buzzard (Nov 19 2019 at 15:46):

So I, J, K, L are the things we knew we needed, and the proofs are relatively straightforward using automation, and then you have some proof which kind of looks awful, although it also looks much shorter than the Lean proof, but it was also found using automation. Thanks Sebastien.

#### Kevin Buzzard (Nov 19 2019 at 15:47):

In particular the proof still looks a bit clunky but it was probably much easier for the user to write.

#### Sebastien Gouezel (Nov 19 2019 at 15:50):

When I write an Isabelle proof I write down enough intermediate statements, and then I ask automation to complete the proof of each intermediate statement, and also to combine them all to prove the main result. If it doesn't work, I add more intermediate statements. This is really different from the way I write Lean proofs (and I think the Isabelle way is much smoother!)

#### Kevin Buzzard (Nov 19 2019 at 15:50):

So now we need to turn this into some sort of concrete proposal(s) for improving Lean.

#### Kevin Buzzard (Nov 19 2019 at 15:51):

Occasionally people pop up and say "I want to write Lean automation, what do you guys need?" and if they're not mathematicians I feel like I can't say "Groebner bases"

#### Kevin Buzzard (Nov 19 2019 at 15:53):

but I can't tell my `cc`

from my `simp`

so I don't feel competent enough to answer a computer scientist. Oh, I know we need a sledgehammer but this seems like a highly non-trivial task. I used to know that we needed `norm_cast`

but now we have that. Imagine how much worse the Lean proof would have been a year ago.

#### Sebastien Gouezel (Nov 19 2019 at 15:54):

What we really need is `auto`

(or `force`

). Something that uses the simplifier but also tries some things that have been marked as reasonable in the library, and backtracks if it doesn't work (with some backtracking depth which is not the same for `auto`

, `fastforce`

and `force`

). This is called a tableau prover, I think.

#### Bryan Gin-ge Chen (Nov 19 2019 at 15:54):

Is it like a stronger version of `tidy`

?

#### Kevin Buzzard (Nov 19 2019 at 15:55):

Out of interest, how long does the automation take to (a) prove I,J,K,L, (b) find the two-line incantation at the end and (c) compile the two-line incantation at the end? Are (a) and (c) super-quick and (b) might take a few minutes?

#### Sebastien Gouezel (Nov 19 2019 at 15:57):

What I also dearly miss is simprocs, i.e., simple algorithms that are used by `simp`

to try to simplify things in addition to the lemmas that have been marked as `simp`

. @Johannes Hölzl had given a start to this, in https://github.com/johoelzl/lean-simp-loop, but I think it never made it into production. For instance, if you see `∃a, a = t ∧ p a`

, you would like to reduce it to `p t`

.

#### Kevin Buzzard (Nov 19 2019 at 15:58):

That's not some lemma in logic.basic which you can just rewrite or something?

#### Kevin Buzzard (Nov 19 2019 at 15:59):

Is it a bad simp lemma?

#### Sebastien Gouezel (Nov 19 2019 at 15:59):

(a) and (c) are instantaneous. (b) takes less than 5 seconds.

#### Sebastien Gouezel (Nov 19 2019 at 16:00):

Johannes also wanted as a simproc to have`∃a, p a ∧ ∃b, ∃h : a = f b, q a h`

transform into `∃b, p (f b) ∧ q (f b) rfl`

, and also all the possible variations. So, it's rather infinitely many lemmas (and many of them would not fire as simp lemmas, yes).

#### Sebastien Gouezel (Nov 19 2019 at 16:02):

Yes, it's a stronger version of `tidy`

(note that `tidy`

never backtracks). `back`

is supposed to do something like that, but I don't know if @Scott Morrison is planning to do it as a tableau prover, i.e., registering what has already been proved and add progressively new facts, to get something efficient.

#### Bhavik Mehta (Nov 19 2019 at 19:24):

If anyone's interested, I've now got it to this (taking a lot from @Mario Carneiro's version) :

lemma nat.choose_succ_right_eq {n k : ℕ} : nat.choose n (k + 1) * (k + 1) = nat.choose n k * (n - k) := begin have e : (n+1) * nat.choose n k = nat.choose n k * (k+1) + nat.choose n (k+1) * (k+1), rw [← nat.right_distrib, ← nat.choose_succ_succ, nat.succ_mul_choose_eq], rw [← nat.sub_eq_of_eq_add e, mul_comm, ← nat.mul_sub_left_distrib], simp end theorem div_le_div_iff {α} [linear_ordered_field α] {a b c d : α} (hc : 0 < c) (hd : 0 < d) : a / c ≤ b / d ↔ a * d ≤ b * c := by rw [le_div_iff hd, div_mul_eq_mul_div, div_le_iff hc] theorem main_lemma {A B n r : ℕ} (hr1 : 1 ≤ r) (hr2 : r ≤ n) (h : A * r ≤ B * (n - r + 1)) : (A : ℚ) / (nat.choose n r) ≤ B / nat.choose n (r-1) := begin rw div_le_div_iff; norm_cast, apply le_of_mul_le_mul_right _, exact hr1, cases r, simp, rw nat.succ_eq_add_one at *, rw [← nat.sub_add_comm hr2, nat.add_sub_add_right] at h, rw [nat.add_sub_cancel, mul_assoc B, nat.choose_succ_right_eq, mul_right_comm, ← mul_assoc, mul_right_comm B], exact nat.mul_le_mul_right _ h, apply nat.choose_pos hr2, apply nat.choose_pos (le_trans (nat.pred_le _) hr2) end

In particular a somewhat quicker proof of `nat.choose_succ_right_eq`

, which doesn't need the assumption either

#### Bhavik Mehta (Nov 19 2019 at 19:25):

I don't *really* like how we do a `cases r`

but it does seem faster

#### Kevin Buzzard (Nov 19 2019 at 19:26):

Your `cases r`

is just my "replace r with s=r-1" right? It's just one less inequality to deal with. If you can start at 0, do.

#### Bhavik Mehta (Nov 19 2019 at 19:30):

It doesn't solve the inequality as far as I can tell - it's just that we state `nat.choose_succ_right_eq`

with lots of `+ 1`

s around, so it's easier to unify when we've `succ`

ed `r`

#### Bhavik Mehta (Nov 19 2019 at 23:53):

A PR for `choose_succ_right_eq`

and another basic choose fact `choose n k = choose n (n-k)`

: https://github.com/leanprover-community/mathlib/pull/1717

#### Johan Commelin (Nov 20 2019 at 08:18):

I see the following line (https://github.com/leanprover-community/mathlib/blob/7ae8b1d6821da5f4018c8c885c88d74e21578a83/src/data/nat/basic.lean#L1086)

lemma succ_mul_choose_eq : ∀ n k, succ n * choose n k = choose (succ n) (succ k) * succ k

Shouldn't that be rewritten to use `(n+1)`

everywhere? I thought `succ`

should be exposed as little as possible.

#### Bhavik Mehta (Nov 21 2019 at 10:17):

`div_le_div_iff`

missing is even more scandalous. I would have expected that in core

PR for this (into algebra/ordered_field): https://github.com/leanprover-community/mathlib/pull/1720

#### Bhavik Mehta (Nov 21 2019 at 10:35):

I see the following line (https://github.com/leanprover-community/mathlib/blob/7ae8b1d6821da5f4018c8c885c88d74e21578a83/src/data/nat/basic.lean#L1086)

lemma succ_mul_choose_eq : ∀ n k, succ n * choose n k = choose (succ n) (succ k) * succ kShouldn't that be rewritten to use

`(n+1)`

everywhere? I thought`succ`

should be exposed as little as possible.

@Johan Commelin Is this a suggestion for the PR, or a general comment?

#### Johan Commelin (Nov 21 2019 at 10:38):

More of a general comment/question

#### Johan Commelin (Nov 21 2019 at 10:38):

I'm still confused about whether this is intended, or whether mathlib drifted to a style where `succ`

is deprecated

Last updated: May 13 2021 at 18:26 UTC