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