proposition: Lemma shiftr_shiftl_r : forall a n m, 0<=n -> (a << n) >> m == a >> (m-n).
proof: Proof. intros. now rewrite <- 2 shiftl_opp_r, shiftl_shiftl, opp_sub_distr, add_comm. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog