n m k : (k * n) mod (k * m) = k * (n mod m). Proof. destruct (nat_zero_or_gt_zero k) as [[] | kp]. 1: reflexivity. destruct (nat_zero_or_gt_zero m) as [[] | mp]. 1: by rewrite nat_mul_zero_r. apply (nat_mod_unique _ _ (n / 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