proposition: Lemma blit_pos :forall a b, Lit.blit a = Lit.blit b -> Lit.is_pos a = Lit.is_pos b -> a = b.
proof: Proof. Proof lsr_is_even_eq. Lemma blit_lit : forall l, blit (lit (blit l)) = blit l. Proof. intros l;case_eq (is_pos l);intros. rewrite lit_blit;trivial. rewrite lit_blit_neg, blit_neg;trivial. Qed.
imports: List Bool Int63 Psatz Ring63 PArray Misc Ring