Commit 2021-01-15 05:41 faf106a3

refactor(data/real/{e,}nnreal): reuse generic lemmas (#5751)

• reuse div_eq_mul_inv and one_div from div_inv_monoid;
• reuse lemmas about group_with_zero instead of repeating them in the nnreal namespace;
• add has_sum.div_const.