proposition: Fact is_gcd_sym p q r : is_gcd p q r -> is_gcd q p r.
proof: Proof. intros (? & ? & ?); repeat split; auto. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)