n m k : (n / m) / k = n / (m * k). Proof. destruct (nat_zero_or_gt_zero k) as [[] | kp]. 1: by rewrite nat_mul_zero_r. destruct (nat_zero_or_gt_zero m) as [[] | mp]. 1: snrapply nat_div_zero_l. apply nat_div_unique with (r := (n mod (m * k)) / m). { apply (lt_lt_leq_trans (m:=(m * k)/m)). - rapply nat_div_strictly_monotone_r. nrapply (nat_mod_lt_r' _ _ 0 _). exact (nat_mul_strictly_monotone mp kp). - by rewrite nat_div_mul_cancel_l. } transitivity ((m * (k * (n / (m * k)))) / m + (n mod (m * k)) / m). - f_ap. symmetry; rapply nat_div_mul_cancel_l. - rewrite nat_mul_assoc. lhs_V nrapply nat_div_dist. 1: exact _. apply (ap (fun x => x / m)). symmetry; apply nat_div_mod_spec. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes