proposition: Lemma shiftl_div_pow2 : forall a n, n<=0 -> a << n == a / 2^(-n).
proof: Proof. intros. bitwise. rewrite shiftl_spec, div_pow2_bits; trivial. - now rewrite add_opp_r. - now apply opp_nonneg_nonpos. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog