WordAuto.v: prove [Ninj_div] & [Ninj_mod]
WordAuto.v: prove [Ninj_div] & [Ninj_mod]

It turns out the behavior of mod actually differs between nat and N
when the divisor is 0, so Ninj_mod needed an extra precondition.
Luckily, the automation seems to have dispatched it everywhere!

mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl