nat_sub_r_add@{} n m k : n - (m + k) = n - m - k. Proof. induction n as [|n IHn] in m, k |- *. - reflexivity. - destruct m. + reflexivity. + nrapply IHn. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids