In this case, to apply strong_induction
you need to change
the conclusion of the goal so that it better matches the conclusion of the theorem.
Goal forall a b, b <> 0 -> exists ! q r, a = q * b + r /\ r < b.
change (forall a, (fun c => forall b, b <> 0 -> exists ! q r, c = q * b + r /\ r < b) a).
eapply strong_induction.
You could also use more directly the refine
tactic. This tactic is similar to the apply
tactic.
Goal forall a b, b <> 0 -> exists ! q r, a = q * b + r /\ r < b.
refine (strong_induction _ _).
But the induction
tactic already handles arbitrary induction principles.
Goal forall a b, b <> 0 -> exists ! q r, a = q * b + r /\ r < b.
induction a using strong_induction.
More on these tactics here. You should probably use induction
before intro
-ing and split
-ing.