proposition: Fact divides_div q p : divides p q -> q = div q p * p.
proof: Proof. intros (k & Hk). destruct (eq_nat_dec p 0) as [ Hp | Hp ]. + subst; do 2 (rewrite Nat.mul_comm; simpl); auto. + rewrite (@div_prop q p k 0); lia. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)