proposition: Lemma Popp_ok P l : (--P)@l == - P@l.
proof: Proof. revert l;induction P as [|p P IHP|P2 IHP1 p P3 IHP2];simpl;intros. - Esimpl. - apply IHP. - rewrite IHP1, IHP2;rsimpl. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory