proposition: Fact nat_lb_1 : ⟬ 1⟭ = ⟙::nil.
proof: Proof. change 1 with (1+2*0). rewrite nat_lb_fix_2, nat_lb_fix_0. trivial. 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)