proposition: Fact divides_mult_compat a b c d : a div b -> c div d -> a*c div b*d.
proof: Proof. intros (u & ?) (v & ?); exists (u*v); subst. repeat rewrite Nat.mul_assoc; f_equal. repeat rewrite <- Nat.mul_assoc; f_equal. apply Nat.mul_comm. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)