proposition: Lemma bit_b2i (b: bool) i : bit b i = (i =? 0)%uint63 && b.
proof: Proof. case b; unfold bit; simpl b2i. - rewrite lsr_1; case (i =? 0)%uint63; auto. - rewrite lsr0, lsl0, andb_false_r; auto. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63