proposition: Fact nat_lb_fix_1 n : n <> 0 -> ⟬ 2*n⟭ = ⟘::⟬ n⟭ .
proof: Proof. intros Hn. apply g_nlb_fun with (2*n); auto. constructor; auto; try lia. + apply rem_2_fix_1. + rewrite div_2_fix_1; 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)