n m k : 0 < n -> (n * m + k) / n = m + k / n. Proof. intros H. rapply (nat_div_unique _ _ _ (k mod n) _). rewrite nat_dist_l. lhs_V nrapply nat_add_assoc. f_ap. symmetry; apply nat_div_mod_spec. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes