What you are saying might make sense in regular programming languages like go/rust/etc but it does not make sense in type theory. Rather the reason that n / 0 =

What you are saying might make sense in regular programming languages like go/rust/etc but it does not make sense in type theory. Rather the reason that n / 0 = 0 makes sense in type theory is that you can simply define types such as (n : Nat) -> (m : Nat) -> Nonzero m -> n / m * m = n as in you do not need to make your laws hold true for every possible input of / which is why it does not break regular mathematics.