proposition: Lemma Pmul_ok P P' l : (P**P')@l == P@l * P'@l.
proof: Proof. revert P l;induction P' as [| |? IHP'1 ? ? IHP'2];simpl;intros P l. - apply PmulC_ok. - apply PmulI_ok;trivial. - destruct P as [|p0|]. + rewrite (ARmul_comm ARth). Esimpl. + Esimpl. rewrite IHP'1;Esimpl. f_equiv. destruct p0;rewrite IHP'2;Esimpl. * now rewrite Pjump_xO_tail. * rewrite Pjump_pred_double; Esimpl. + rewrite Padd_ok, !mkPX_ok, Padd_ok, !mkPX_ok, !IHP'1, !IHP'2, PmulI_ok; trivial. simpl. Esimpl. unfold tail. add_permut; f_equiv; mul_permut. Qed.
imports: Setoid Morphisms Env BinPos BinNat BinInt Ring_theory