proposition: Fact is_gcd_mult p q r n : is_gcd p (n*p+q) r <-> is_gcd p q r.
proof: Proof. split. + replace q with ((n*p+q)-n*p) at 2 by lia. apply is_gcd_modulus; auto; lia. + rewrite Nat.add_comm; apply is_gcd_moduplus; auto. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)