mathlib3

e22fb94e - chore(data/nat/cast,algebra/ordered_group): 2 trivial lemmas (#5436)