proposition: Theorem nat_iter_add (n m : nat) {A} (f : A -> A) (x : A) : nat_iter (n + m) f x = nat_iter n f (nat_iter m f x).
proof: Proof. simple_induction n n IHn; simpl; trivial. exact (ap f IHn). Defined.
imports: Basics Types Basics.Nat HoTT.DProp