Nat.strong_induction_on vs Nat.strongRecOn

Stream: mathlib4

[Jeremy Tan]

In #16464 I deprecate Nat.(case_)strong_induction_on in Data.Nat.Defs for their equivalents in core, named Nat.(cases)strongRecOn.

@Johan Commelin then prodded me to ask here whether keeping the versions with induction in them would be warranted for discoverability purposes, so here is this thread

[Jireh Loreaux]

yes, I think we should keep the induction variants for discoverability.

[Violeta Hernández]

Agree, they should probably be aliases instead though