proposition: Lemma shiftr_ldiff : forall a b n, (ldiff a b) >> n == ldiff (a >> n) (b >> n).
proof: Proof. intros. bitwise. now rewrite !shiftr_spec, ldiff_spec. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog