proposition: Lemma lit_blit_neg: forall l, is_pos l = false -> lit (blit l) = neg l.
proof: Proof. unfold is_pos, lit, blit;intros. rewrite (bit_xor_split l) at 2. rewrite is_even_bit, negb_false_iff in H;rewrite H. rewrite <- (neg_involutive ((l >> 1) << 1)) at 1;trivial. Qed.
imports: List Bool Int63 Psatz Ring63 PArray Misc Ring