proposition: Lemma lsr_1 n : 1 >> n = (n =? 0)%uint63.
proof: Proof. case eqbP. - intros h; rewrite (to_Z_inj _ _ h), lsr_0_r; reflexivity. - intros Hn. assert (H1n : (1 >> n = 0)%uint63); auto. apply to_Z_inj; rewrite lsr_spec. apply Zdiv_small; rewrite to_Z_1; split; auto with zarith. change 1%Z with (2^0)%Z. apply Zpower_lt_monotone; split; auto with zarith. rewrite to_Z_0 in Hn. generalize (to_Z_bounded n). lia. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63