b Properties

In this file we introduce some generally helpful lemmas for b.

References

See [bernstein2013a], Section 3.4, Theorem 4.

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

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

theorem Elligator.Elligator1.two_pow_b_gt_q_div_two {q : ℕ} : 2 ^ b q > q / 2

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