proposition: Fact lb_succ_bot l : lb_succ ⟘ l ≂ l.
proof: Proof. induction l as [ | x ]; simpl; auto. + split; repeat constructor. + destruct x; rewrite IHl; 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)