feat (data/list/basic): lemmas about prod and take (#2345)
* feat (data/list/basic): lemmas about prod and take
* move lemma
* one more
* using to_additive properly
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
