Commit 2023-11-12 23:30 4cb02b43

feat: add aesop attribute to Nat.not_prime_one (#8332) @Yaël Dillies's recent proof at #8164 uses aesop in a way that relies on simp using decide := true by default, which we have now disabled, and hence this breaks on nightly-testing. I propose we add @[aesop safe destruct] to Nat.not_prime_one (and Nat.not_prime_zero while we're there).