proposition: Lemma bit_split i : ( i = (i >> 1 ) << 1 + bit i 0)%uint63.
proof: Proof. apply to_Z_inj. rewrite -> add_spec, lsl_spec, lsr_spec, bit_0_spec, Zplus_mod_idemp_l. replace (2 ^ φ 1) with 2%Z; auto with zarith. rewrite -> Zmult_comm, <-Z_div_mod_eq_full. rewrite Zmod_small; auto; case (to_Z_bounded i); auto. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63