proposition: Lemma strong_rec0_fixpoint : forall (a : A) (n : N.t), Aeq (strong_rec0 a f (S n) n) (f (fun n => strong_rec0 a f (S n) n) n).
proof: Proof. intros. rewrite strong_rec0_succ. apply step_good. intros m Hm. symmetry. setoid_replace n with (S m + (n - S m)). - apply strong_rec0_more_steps. apply lt_succ_diag_r. - rewrite add_comm. symmetry. apply sub_add. rewrite le_succ_l; auto. Qed.
imports: NSub