proposition: Lemma lnot_shiftr : forall a n, 0<=n -> lnot (a >> n) == (lnot a) >> n.
proof: Proof. intros a n Hn. bitwise. now rewrite lnot_spec, 2 shiftr_spec, lnot_spec by order_pos. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog