proposition: Lemma lxor_lsr i1 i2 i: (i1 lxor i2) >> i = (i1 >> i) lxor (i2 >> i).
proof: Proof. apply bit_ext; intros n. rewrite lxor_spec, !bit_lsr, lxor_spec. case (_ <=? _); auto. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz