proposition: Fact nat_pow2_lb_shift n q : ⟬q*power n 2⟭ ≂ lb_shift n ⟬q⟭ .
proof: Proof. apply lb_mask_equiv_equal. rewrite lb_nat_lb, lb_nat_shift, lb_nat_lb; 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)