n m : n / m = (n - n mod m) / m. Proof. destruct (nat_zero_or_gt_zero m) as [[] | mp]. 1: reflexivity. symmetry. rewrite nat_div_mod_spec''. rapply nat_div_mul_cancel_l. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes