proposition: Lemma lit_blit: forall l, is_pos l = true -> lit (blit l) = l.
proof: Proof. unfold is_pos, lit, blit;intros. rewrite (bit_xor_split l) at 2. rewrite is_even_bit, negb_true_iff in H;rewrite H. symmetry;apply lxor0_r. Qed.
imports: List Bool Int63 Psatz Ring63 PArray Misc Ring