proposition: Fact divides_rem_eq q p : divides p q <-> rem q p = 0.
proof: Proof. destruct (eq_nat_dec p 0) as [ Hp | Hp ]. * subst; rewrite rem_0; split. + apply divides_0_inv. + intros; subst; apply divides_0. * split. + intros (n & Hn). apply rem_prop with n; lia. + intros H. generalize (div_rem_spec1 q p). exists (div q p); lia. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)