Ch01: add lemma for proof 4

[rwst]

There might be improvements to prod_Icc_succ_div that I don't see. I also think this should go in mathlib to the other prod lemmata. What do you say, will you take it as is? If not, I'll try again.

[mo271]

Thanks, this looks great!

[mo271]

There might be improvements to prod_Icc_succ_div that I don't see. I also think this should go in mathlib to the other prod lemmata. What do you say, will you take it as is? If not, I'll try again.

Seems like there is Finset.prod_Ico_succ_div_top but genereally it seems like there is more lemmata for Ico than for Icc in mathlib. I don't know if this is by design or they are just missing and waiting to be added. Best ask at Zulip if you have a concrete suggestion.

[mo271]

Thanks!