proposition: Fact is_gcd_0 p q : is_gcd p q 0 -> p = 0 /\ q = 0.
proof: Proof. intros ((a & Ha) & (b & Hb) & H). subst; do 2 rewrite Nat.mul_0_r; auto. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)