proposition: Theorem recursion_succ : forall {A} (Aeq : relation A) (a : A) (f : nat -> A -> A), Aeq a a -> Proper (eq==>Aeq==>Aeq) f -> forall n : nat, Aeq (recursion a f (S n)) (f n (recursion a f n)).
proof: Proof. unfold Proper, respectful in *. intros A Aeq a f ? ? n. induction n; simpl; auto. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass