proposition: Lemma bit_xor_split: forall i : int, i = (i >> 1) << 1 lxor bit i 0.
proof: Proof. intros. rewrite bit_or_split at 1. apply lsr_is_even_eq. rewrite lxor_lsr, lor_lsr, lsr1_bit, lxor0_r, lor0_r;trivial. rewrite is_even_or, is_even_xor. rewrite is_even_lsl_1;trivial. rewrite (xorb_true_l (is_even (bit i 0))), negb_involutive;trivial. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz