proposition: Fact divides_bool_spec' n p : divides_bool (S n) p = false <-> ~ S n <d p.
proof: Proof. rewrite <- divides_bool_spec. destruct (divides_bool (S n) p); now split. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat gcd sums)