proposition: Fact divides_minus p q1 q2 : p div q1 -> p div q2 -> p div q1 - q2.
proof: Proof. intros (s1 & H1) (s2 & H2). exists (s1 - s2). rewrite Nat.mul_sub_distr_r; lia. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)