proposition: Fact is_gcd_modulus p q k r : p div k -> k <= q -> is_gcd p q r -> is_gcd p (q-k) r.
proof: Proof. intros (n & Hn) Hq (H1 & H2 & H3); subst. split; auto. split. + apply divides_minus; auto. + intros k H4 H5. apply H3; auto. replace q with (q - n*p + n*p) by lia. apply divides_plus; auto. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)