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