proposition: Fact is_gcd_moduplus p q k r : p div k -> is_gcd p q r -> is_gcd p (q+k) r.
proof: Proof. intros (n & Hn) (H1 & H2 & H3); subst. repeat (split; auto). intros k H4 H5. apply H3; auto. rewrite Nat.add_comm in H5. apply divides_plus_inv with (2 := H5); auto. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)