proposition: Lemma shiftl_spec_alt : forall a n m, 0<=n -> (a << n).[m+n] = a.[m].
proof: Proof. intros. now rewrite shiftl_mul_pow2, mul_pow2_bits, add_simpl_r. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog