proposition: Fact is_gcd_rem p n a : is_gcd p n a <-> is_gcd p (rem n p) a.
proof: Proof. rewrite (div_rem_spec1 n p) at 1; apply is_gcd_mult. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)