n m : n mod m = 0 <-> (m | n) . Proof. split. 2: exact (nat_mod_divides _ _). intros p. exists (n / m). rewrite nat_mul_comm. lhs_V nrapply nat_add_zero_r. rewrite <- p. symmetry. nrapply nat_div_mod_spec. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes