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