proposition: Fact divides_plus_inv p q1 q2 : p div q1 -> p div q1+q2 -> p div q2.
proof: Proof. intros H1 H2. replace q2 with (q1+q2-q1) by lia. apply divides_minus; auto. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)