proposition: Lemma bit_lsr x i j : (bit (x >> i) j = if j <=? i + j then bit x (i + j) else false)%uint63.
proof: Proof. unfold bit; rewrite lsr_add; case (_ ≤? _); auto. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63