proposition: Fact lb_plus_fix_2 a x y l m : lb_plus a (x::l) (y::m) = let (r,z) := bin_add a x y in z::lb_plus r l m.
proof: Proof. auto. Qed.
imports: Arith Nat Lia List Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat bool_list gcd sums power_decomp)