proposition: Lemma spec_lxor: forall x y, to_Z (lxor x y) = Z.lxor (to_Z x) (to_Z y).
proof: Proof. intros x y. unfold lxor. destr_norm_pos x; destr_norm_pos y; simpl; rewrite ?NN.spec_succ, ?NN.spec_lxor, ?NN.spec_pred, ?Z.max_r, ?Zlnot_alt1; auto with zarith. now rewrite !Z.lnot_lxor_r, Zlnot_alt2. now rewrite !Z.lnot_lxor_l, Zlnot_alt2. now rewrite <- Z.lxor_lnot_lnot, !Zlnot_alt2. Qed.
imports: ZArith Lia BigNumPrelude NSig ZSig