proposition: Lemma lxor_lor : forall a b, land a b == 0 -> lxor a b == lor a b.
proof: Proof. intros a b H. bitwise as m. assert (a.[m] && b.[m] = false) by now rewrite <- land_spec, H, bits_0. now destruct a.[m], b.[m]. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog