mathlib3

cd2230b4 - chore(data/nat/prime): golf some proofs (#10599)