proposition: Lemma shiftr_shiftr : forall a n m, 0<=m -> (a >> n) >> m == a >> (n+m).
proof: Proof. intros a n p Hn. bitwise. rewrite 3 shiftr_spec; trivial. - now rewrite (add_comm n p), add_assoc. - now apply add_nonneg_nonneg. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog