proposition: Lemma spec_shiftl: forall x p, to_Z (shiftl x p) = Z.shiftl (to_Z x) (to_Z p).
proof: Proof. intros x p. unfold shiftl. destr_norm_pos x; destruct p as [p|p]; simpl; assert (Hp := NN.spec_pos p). apply NN.spec_shiftl. rewrite Z.shiftl_opp_r. apply NN.spec_shiftr. rewrite !NN.spec_shiftl. rewrite !Z.shiftl_mul_pow2 by apply NN.spec_pos. symmetry. apply Z.mul_opp_l. rewrite Z.shiftl_opp_r, NN.spec_succ, NN.spec_shiftr, NN.spec_pred, Z.max_r by auto with zarith. now rewrite Zlnot_alt1, Z.lnot_shiftr, Zlnot_alt2. Qed.
imports: ZArith Lia BigNumPrelude NSig ZSig