proposition: Fact lb_plus_spec_0 l m : ⟦l⊕m⟧ = ⟦l⟧ + ⟦m⟧.
proof: Proof. rewrite lb_plus_spec; simpl; 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)