proposition: Lemma shiftl_lxor : forall a b n, (lxor a b) << n == lxor (a << n) (b << n).
proof: Proof. intros a b n. bitwise as m. destruct (le_gt_cases n m). - now rewrite !shiftl_spec_high', lxor_spec. - now rewrite !shiftl_spec_low. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog