proposition: Lemma shiftl_lxor : forall a b n, (lxor a b) << n == lxor (a << n) (b << n).
proof: Proof. intros. bitwise. now rewrite !shiftl_spec, lxor_spec. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog