Where can you put the quantifier in Induction

Stream: new members

[Johannes C. Mayer]

Let's assume I want to show.
∀ a, b, c, ab = ac → b = c

With induction on c I would need to show the base case:
∀ a, b, ab = a*0 → b = 0

And then show the inductive case, which I think is defined like this (this seems to be what lean is doing):

∀ a, b, d,
  (ab = ad → b = d) →
  (ab = a(d+1) → b = d+1)

My question is if you could also define induction such that you would need to show this instead (or would this lead to contradictions):

∀ d,
  (∀ a, b, ab = ad → b = d) →
  (∀ a, b, ab = a(d+1) → b = d+1)

[Patrick Johnson]

That's what generalizing is for: induction c generalizing a b does exactly what you want. Alternatively, you can do revert a b and then use induction.

[Johannes C. Mayer]

Thanks, I think I get it now. Induction is defined like I thought and generalizing it like you said, actually changes completely the meaning of the induction hypothesis.

[Kwame Porter Robinson]

Is that strong induction? I think you can do revert a, revert b or use induction ... generalization a b