proposition: Lemma nat_rect_succ_r {A} (f: A -> A) (x:A) n : nat_rect (fun _ => A) x (fun _ => f) (S n) = nat_rect (fun _ => A) (f x) (fun _ => f) n.
proof: Proof. induction n as [|n IHn]; intros; simpl; rewrite <- ?IHn; trivial. Qed.
imports: Notations Ltac Datatypes Logic