proposition: Fact power_2_minus_1 n : power (S n) 2 - 1 = 1 + 2*(power n 2 - 1).
proof: Proof. rewrite power_S. generalize (@power_ge_1 n 2); intros; lia. 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)