fact: Fixpoint lb_nat (l : lb) := match l with | nil => 0 | x :: l => bool2nat x + 2*⟦l⟧ end where "⟦ l ⟧" := (lb_nat l).
imports: Arith Nat Lia List Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat bool_list gcd sums power_decomp)