proposition: Lemma PmulC_aux_ok c P l : (PmulC_aux P c)@l == P@l * [c].
proof: Proof. revert l;induction P as [| |? IHP1 ? ? IHP2];simpl;intros;Esimpl;trivial. rewrite IHP1, IHP2;rsimpl. add_permut. mul_permut. Qed.
imports: Setoid Morphisms Env BinPos BinNat BinInt Ring_theory