proposition: Lemma bitE i j : bit i j = Z.testbit φ(i) φ(j).
proof: Proof. symmetry; apply negb_sym; rewrite is_zeroE, lsl_spec, lsr_spec. generalize (φ i) (to_Z_bounded i) (φ j) (to_Z_bounded j); clear i j; intros i [hi hi'] j [hj hj']. rewrite Z.testbit_eqb by auto; rewrite <- Z_oddE, Z.negb_odd, Z_evenE. remember (i / 2 ^ j) as k. change wB with (2 * 2 ^ φ (digits - 1)). unfold Z.modulo at 2. generalize (Z_div_mod_full k 2 (λ k, let 'eq_refl := k in I)); unfold Remainder. destruct Z.div_eucl as [ p q ]; intros [hk [ hq | ]]. 2: lia. rewrite hk. remember φ (digits - 1) as m. replace ((_ + _) * _) with (q * 2 ^ m + p * (2 * 2 ^ m)) by ring. rewrite Z_mod_plus by (subst m; reflexivity). assert (q = 0 ∨ q = 1) as D by lia. destruct D; subst; reflexivity. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63