Fixpoint natminusminusassoc m n k : (m-n)-k = m-(n+k). Proof. intros. destruct m. { reflexivity. } { destruct n. { rewrite natminuseqn. reflexivity. } { simpl. apply natminusminusassoc. } } Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.