proposition: Lemma bit_ext i j : (forall n, bit i n = bit j n) -> i = j.
proof: Proof. case (to_Z_bounded j); case (to_Z_bounded i). unfold wB; revert i j; elim size. - simpl; intros i j ???? _; apply to_Z_inj; lia. - intros n ih i j. rewrite Nat2Z.inj_succ, Z.pow_succ_r by auto with zarith. intros hi1 hi2 hj1 hj2 hext. rewrite (bit_split i), (bit_split j), hext. do 2 f_equal; apply ih; clear ih. 1, 3: apply to_Z_bounded. 1, 2: now rewrite lsr_spec; apply Z.div_lt_upper_bound. intros b. case (Zle_or_lt φ digits φ b). + rewrite <- leb_spec; intros; rewrite !bit_M; auto. + rewrite <- ltb_spec; intros; rewrite !bit_half; auto. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63