proposition: Fact lb_shift_S n l : lb_shift (S n) l = ⟘ :: lb_shift n l.
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)