proposition: Fact divides_is_gcd a b c : divides a b -> is_gcd b c 1 -> is_gcd a c 1.
proof: Proof. intros H1 H2; msplit 2; try apply divides_1. intros k H3 H4. apply H2; auto. apply divides_trans with a; auto. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)