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