proposition: Fact divides_dec q p : { k | q = k*p } + { ~ divides p q }.
proof: Proof. destruct (eq_nat_dec p 0) as [ Hp | Hp ]. + destruct (eq_nat_dec q 0) as [ Hq | Hq ]. * left; subst; exists 1; auto. * right; contradict Hq; subst; auto. + destruct (@euclid q p Hp) as (n & [ | r ] & H1 & H2). * left; exists n; subst; rewrite Nat.add_comm; auto. * right; intros (m & Hm). rewrite <- Nat.add_0_r in Hm. rewrite Hm in H1. destruct (div_rem_uniq _ _ Hp H1); lia. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)