proposition: Lemma bezout_nc p q : is_gcd p q 1 -> exists a b, a*p+b*q = 1+p*q.
proof: Proof. intros H. destruct bezout_rel_prime with (1 := H) as (a & b & ?). exists a, b; auto. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)