nat_div_div_r' n m k : n / (m / k) = (n * k) / (m - m mod k). Proof. rewrite (nat_div_sub_mod m k). rapply nat_div_div_r. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes