Autogenerate lemmas about `OfNat.ofNat`

Add a command or an attribute that generates lemmas about OfNat.ofNat from lemmas about Nat.cast.

The initial version should work if the original lemma has exactly one argument n of type Nat.
It should:

• add [n.AtLeastTwo] assumption;
• replace all occurrences of Nat.cast n with OfNat.ofNat n;
• drop the following assumptions proving them using [n.AtLeastTwo]:
  • n ≠ 0
  • 0 < n
  • n ≠ 1
  • 1 < n
  • 2 ≤ n
• prove the resulting lemma by defeq to the old lemma;
• in case of a simp lemma, add no_index as needed;
• find one of nat_cast or natCast or coe_nat or nat_coe or nat in the name and replace it with ofNat.

Optional features:

• deal with two natural numbers (should we replace both with ofNat or generate 3 versions?)
• allow some customization (not sure what will be needed in real life).

Start by reviewing the existing lemmas about Nat.cast and the command or attribute mechanisms available for generating declarations. Define the initial scope around one Nat argument: add the AtLeastTwo assumption, perform the substitutions and assumption proofs, preserve simp behavior, prove by defeq, and rename the generated lemma. Treat the two-natural-number and customization ideas as out of scope unless clarified.