proposition: Fact lb_nat_shift n l : ⟦lb_shift n l⟧ = ⟦l⟧*power n 2.
proof: Proof. unfold lb_shift. induction n as [ | n IHn ]; simpl lb_bots. + rewrite power_0; simpl; ring. + simpl app; rewrite lb_nat_fix_1, IHn, power_S; ring. 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)