n m k : 0 < k -> (k * n) / (k * m) = n / m. Proof. intro kp. destruct (nat_zero_or_gt_zero m) as [[] | mp]. 1: by rewrite nat_mul_zero_r. nrapply (nat_div_unique _ _ _ (k * (n mod m))). 1: rapply nat_mul_l_strictly_monotone. rewrite <- nat_mul_assoc. rewrite <- nat_dist_l. apply ap. symmetry; apply nat_div_mod_spec. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes