proposition: Fact power_2_minus_1_gt n x : x < power n 2 <-> x ≲ power n 2 - 1.
proof: Proof. split. 2: { intro Hx. apply binary_le_le in Hx. generalize (@power_ge_1 n 2); intros; lia. } intros H1. assert (x <= power n 2 -1) as H by lia; clear H1. rewrite binary_le_nat_meet. revert x H; induction n as [ | n IHn ]; intros x Hx. + rewrite power_0 in Hx; replace x with 0; auto; lia. + destruct (eq_nat_dec x 0) as [ H | H ]. - rewrite H; auto. - destruct (euclid_2_div x) as (H1 & H2). rewrite H1, power_2_minus_1. rewrite nat_meet_euclid_2; try lia. rewrite IHn. * f_equal; destruct H2 as [ H2 | H2 ]; rewrite H2; auto. * rewrite power_2_minus_1 in Hx; 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)