Commit 2024-07-13 07:32 ce2899f1

feat: a replacement for Nat.leRecOn' that works with induction (#14431) Before this PR, we had:

• theorem Nat.le.rec: induct on a ≤ b, but using an annoying a.le b spelling
• theorem Nat.le_induction: induct on a ≤ b
• def Nat.leRecOn', which is Nat.le.rec that works in Sort* but does not work with the induction keyword. There are no lemmas about this definition.
• def Nat.leRecOn, a weaker version of Nat.leRecOn' that also doesn't work with induction. There are lots of lemmas about this definition This PR introduces Nat.leRec, which is a Sort*-valued version of Nat.le.rec, with a signature that coincides in the Prop case. Where appropriate, the lemmas about Nat.leRecOn are recovered as special cases of lemmas about this new definition. Nat.leRecOn' is then deprecated, as it is strictly less useful than Nat.leRec. This also changes the signature of Nat.decreasingInduction to be usable with the induction tactic, with no deprecated alias since there are very few uses. Nat.decreasingInduction' is left alone, as it is unclear to me how to state it in a way understood by induction.