proposition: Lemma lor_lsr i1 i2 i: (i1 lor i2) >> i = (i1 >> i) lor (i2 >> i).
proof: Proof. apply bit_ext; intros n. rewrite -> lor_spec, !bit_lsr, lor_spec. case (_ <=? _)%uint63; auto. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63