proposition: Lemma spec_shiftr: forall x p, [shiftr x p] = Z.shiftr [x] [p].
proof: Proof. intros. now rewrite spec_shiftr_pow2, Z.shiftr_div_pow2 by apply spec_pos. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen