Commit 2024-12-22 10:16 e731cb89

chore: deprecate Nat.cast_eq_ofNat (#20168) This lemma is malformed; the n on the RHS must be a raw literal, but the one on the left is not. Correcting the statement results in Nat.cast_ofNat which already exists.