proposition: Lemma lsr_add i m n: ((i >> m) >> n = if n <=? m + n then i >> (m + n) else 0)%uint63.
proof: Proof. case (to_Z_bounded m); intros H1m H2m. case (to_Z_bounded n); intros H1n H2n. case (to_Z_bounded i); intros H1i H2i. generalize (add_le_r m n); case (n <=? m + n)%uint63; intros H. - apply to_Z_inj; rewrite -> !lsr_spec, Zdiv_Zdiv, <- Zpower_exp; auto with zarith. rewrite add_spec, Zmod_small; auto with zarith. - apply to_Z_inj; rewrite -> !lsr_spec, Zdiv_Zdiv, <- Zpower_exp; auto with zarith. apply Zdiv_small. split; [ auto with zarith | ]. eapply Z.lt_le_trans; [ | apply Zpower2_le_lin ]; auto with zarith. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63