proposition: Theorem nat_rect_plus : forall (n m:nat) {A} (f:A -> A) (x:A), nat_rect (fun _ => A) x (fun _ => f) (n + m) = nat_rect (fun _ => A) (nat_rect (fun _ => A) x (fun _ => f) m) (fun _ => f) n.
proof: Proof. intro n; induction n as [|n IHn]; intros; simpl; rewrite ?IHn; trivial. Qed.
imports: Notations Ltac Datatypes Logic