fact: Fixpoint lb_bots n := match n with | 0 => nil | S n => ⟘ :: lb_bots n end.
imports: Arith Nat Lia List Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat bool_list gcd sums power_decomp)