proposition: Lemma strong_rec0_more_steps : forall a k n m, m < n -> Aeq (strong_rec0 a f n m) (strong_rec0 a f (n+k) m).
proof: Proof. intros a k n. pattern n. apply induction; clear n. - intros n n' Hn; setoid_rewrite Hn; auto with *. - intros m Hm. destruct (nlt_0_r _ Hm). - intros n IH m Hm. rewrite lt_succ_r in Hm. rewrite add_succ_l. rewrite 2 strong_rec0_succ. apply step_good. intros m' Hm'. apply IH. apply lt_le_trans with m; auto. Qed.
imports: NSub