> Lean can deduce proofs implicitly as well.

Sure, but you still have to explicitly ask it to.

> What is a standard subtraction over natural numbers at all?

If you need something that is always defined then you have to use a non-standard subtraction (i.e. saturating subtraction). In other words the `-` operator should not work for Nat. It should require you to use `-_`.