proposition: Lemma asr_1 (n : int) : (1 >> n)%sint63 = (n =? 0)%sint63.
proof: Proof. apply to_Z_inj; rewrite asr_spec. case eqbP; [> now intros -> | intros neqn0]. case (lebP 0 n). - intros le0n. apply Z.div_1_l; apply Z.pow_gt_1; [> easy |]. rewrite to_Z_0 in *; lia. - rewrite Z.nle_gt; intros ltn0. now rewrite Z.pow_neg_r. Qed.
imports: ZArith Uint63 Lia