theorem Elligator.Elligator1.image_of_bitsToNat_of_S_eq_icc_zero_to_q_sub_one_over_two {q : ℕ} : Finset.image bitsToNat S = Finset.Icc 0 ((q - 1) / 2)

theorem Elligator.Elligator1.S_card_eq_icc_zero_to_q_sub_one_over_two_card {q : ℕ} : S.card = (Finset.Icc 0 ((q - 1) / 2)).card

theorem Elligator.Elligator1.S_card_eq_q_add_one_over_two {q : ℕ} (q_mod_4_congruent_3 : q % 4 = 3) : S.card = (q + 1) / 2