n m : (m | n) -> n mod m = 0. Proof. intros [x p]. destruct p. destruct m. { simpl. apply nat_mul_zero_r. } lhs_V nrapply nat_div_mod_spec'. rewrite nat_div_mul_cancel_r; only 2: exact _. apply nat_moveR_nV, nat_mul_comm. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes