proposition: Fact nat_lb_plus n m : ⟬n+m⟭ ≂ ⟬n⟭⊕⟬m⟭.
proof: Proof. rewrite lb_mask_equiv_equal, lb_nat_lb, lb_plus_spec_0. f_equal; symmetry; apply lb_nat_lb. 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)