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