proposition: Lemma blit_nlit : forall l, blit (nlit (blit l)) = blit l.
proof: Proof. intros l;case_eq (is_pos l);intros. rewrite nlit_blit_neg, blit_neg;trivial. rewrite nlit_blit;trivial. Qed.
imports: List Bool Int63 Psatz Ring63 PArray Misc Ring