proposition: Proposition natminuspluseq' (n m : nat) : n <= m -> n + (m - n) = m.
proof: Proof. intros. destruct (symmetric_paths _ _ (nat_add_comm n (m - n))). apply natminuspluseq. assumption. Defined.
imports: Basics Spaces.Nat.Core