n m k : (k | m) -> n / (m / k) = (n * k) / m. Proof. intros [d r]. destruct (nat_zero_or_gt_zero k) as [[] | kp]. 1: by rewrite nat_mul_zero_r, nat_div_zero_l. destruct r. rhs nrapply nat_div_cancel_mul_r. 2: exact _. apply ap. rapply nat_div_mul_cancel_r. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes