n m : (n | m) -> (m / n) * n = m. Proof. destruct n. { intros [k []]. cbn. symmetry; apply nat_mul_zero_r. } intros [k []]. f_ap. rapply nat_div_mul_cancel_r. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes