mathlib

cc20a865 - feat(data/nat/basic): `simp` lemmas about inequalities with `bit*` (#2207)

feat(data/nat/basic): `simp` lemmas about inequalities with `bit*` (#2207) * feat(data/nat/basic): `simp` lemmas about inequalities with `bit*` * Fix compile of `computability/partrec_code` * Fix `nat.bit_cases` to work for `Type*` too * Generalize some lemmas to `linear_ordered_semiring`s * Apply suggestions from code review Co-Authored-By: Gabriel Ebner <gebner@gebner.org> * Apply suggestions from code review Co-Authored-By: Scott Morrison <scott@tqft.net> * fixing a proof Co-authored-by: Gabriel Ebner <gebner@gebner.org> Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>