proposition: Lemma bit_half i n (H: (n <? digits = true)%uint63) : bit (i>>1) n = bit i (n+1).
proof: Proof. unfold bit. rewrite lsr_add. case_eq (n <=? (1 + n))%uint63. - replace (1+n)%uint63 with (n+1)%uint63; [auto|idtac]. apply to_Z_inj; rewrite !add_spec, Zplus_comm; auto. - intros H1; assert (H2: n = max_int). 2: generalize H; rewrite H2; discriminate. case (to_Z_bounded n); intros H1n H2n. case (Zle_lt_or_eq φ n (wB - 1)); auto with zarith; intros H2; apply to_Z_inj; auto. generalize (add_le_r 1 n); rewrite H1. change φ max_int with (wB - 1)%Z. replace φ 1 with 1%Z; auto with zarith. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63