fact: Fixpoint lb_plus a l m := match l, m with | nil, m => lb_succ a m | l, nil => lb_succ a l | x::l, y::m => let (r,z) := bin_add a x y in z::lb_plus r l m end.
imports: Arith Nat Lia List Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat bool_list gcd sums power_decomp)