proposition: Lemma shiftr_mul_pow2 : forall a n, n<=0 -> a >> n == a * 2^(-n).
proof: Proof. intros. bitwise. rewrite shiftr_spec, mul_pow2_bits; trivial. - now rewrite sub_opp_r. - now apply opp_nonneg_nonpos. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog