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