proposition: Proposition nataddsub_assoc_implication (n : nat) {m k z : nat} : (k <= m) -> n + (m - k) = z -> n + m - k = z.
proof: Proof. intro H. destruct (symmetric_paths _ _ (nataddsub_assoc n H)); done. Defined.
imports: Basics Spaces.Nat.Core