theorem Elligator.Elligator1.two_pow_b_le_q {q : ℕ} (q_mod_4_congruent_3 : q % 4 = 3) : 2 ^ b ≤ q

theorem Elligator.Elligator1.q_lt_two_pow_b_succ {q : ℕ} : q < 2 ^ (b + 1)

theorem Elligator.Elligator1.two_pow_b_gt_q_over_two {F : Type u_1} [Field F] [Fintype F] {q : ℕ} (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : 2 ^ b > q / 2

theorem Elligator.Elligator1.half_q_lt_two_pow_b {q : ℕ} : (q - 1) / 2 < 2 ^ b