proposition: Proposition subsubadd (n m k : nat) : n - (m + k) = n - m - k.
proof: Proof. revert m k; simple_induction n n IHn. - reflexivity. - intro m; destruct m; intro k. + change (0 + k) with k; reflexivity. + change (m.+1 + k) with (m + k).+1; apply IHn. Defined.
imports: Basics Spaces.Nat.Core