title: Coq: adding a "strong induction" tactic
body: <p>"Strong" (or "complete") induction on the natural number means that when proving the induction step on n, you can assume the property holds for any k
  
  <pre><code>Theorem strong_induction:
  forall P : nat -&gt; Prop,
  (forall n : nat, (forall k : nat, (k &lt; n -&gt; P k)) -&gt; P n) -&gt;
  forall n : nat, P n.
  </code></pre>
  
  <p>I have managed to prove this theorem without too many difficulties. Now I want to use it in a new tactic, strong_induction, which should be similar to the standard "induction n" technique on the natural numbers. Recall that when using "induction n" when n is a natural number and the goal is P(n), we get two goals: One of the form P(0) and the second of the form P(S(n)), where for the second goal we get P(n) as assumption.</p>
  
  <p>So I want, when the current goal is P(n), to get one new goal, also P(n), but the new assumption "forall k : nat, (k &lt; n -> P(k)))".</p>
  
  <p>The problem is I don't know how to do it technically. My main problem is this: Suppose P is a complex statement, i.e. </p>
  
  <pre><code>exists q r : nat, a = b * q + r
  </code></pre>
  
  <p>with a b : nat in the context; how can I tell Coq to do the strong induction on a and not on b? simply doing "apply strong_induction" results in</p>
  
  <pre><code>n : nat
  H0 : forall k : nat, k &lt; n -&gt; exists q r : nat, a = b * q + r
  ______________________________________(1/2)
  exists q r : nat, a = b * q + r
  ______________________________________(2/2)
  nat
  </code></pre>
  
  <p>where the assumption is useless (since n does not relate to a) and I have no idea what the second goal means.</p>