k : 0 < k -> IsInjective (fun n => nat_mul n k). Proof. intros kp m n p. lhs_V rapply (nat_div_mul_cancel_r _ k). rhs_V rapply (nat_div_mul_cancel_r _ k). exact (ap (fun x => x / k) p). Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes