mathlib3

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