{N : SuccStr} (n : N) (k l : nat) : n + (k + l) = (n + l) + k := nat_iter_add k l ss_succ n.
Require Import Basics. Require Import Nat.Core. Require Import Spaces.Int. Require Import Spaces.Finite.Fin. Require Import WildCat.Core.