fact: Definition bezout_rel_prime_lt p q : 0 < p < q -> is_gcd p q 1 -> { a : nat & { b | a*p+b*q = 1+p*q /\ a <= q /\ b <= p } }.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)