proposition: Lemma lsr_M_r x i (H: (digits <=? i = true)%uint63) : x >> i = 0%uint63.
proof: Proof. apply to_Z_inj. rewrite lsr_spec, to_Z_0. case (to_Z_bounded x); intros H1x H2x. case (to_Z_bounded digits); intros H1d H2d. rewrite -> leb_spec in H. apply Zdiv_small; split; [ auto | ]. apply (Z.lt_le_trans _ _ _ H2x). unfold wB; change (Z_of_nat size) with φ digits. apply Zpower_le_monotone; auto with zarith. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63