proposition: Lemma PmulI_ok P' : (forall P l, (Pmul P P') @ l == P @ l * P' @ l) -> forall P p l, (PmulI Pmul P' p P) @ l == P @ l * P' @ (jump p l).
proof: Proof. intros IHP' P. induction P as [|p P IHP|? IHP1 ? ? IHP2];simpl;intros p0 l. - Esimpl; mul_permut. - destr_pos_sub; intros ->;Esimpl. + now rewrite IHP'. + now rewrite IHP', jump_add'. + now rewrite IHP, jump_add'. - destruct p0;Esimpl; rewrite ?IHP1, ?IHP2; rsimpl. + f_equiv. mul_permut. + rewrite jump_pred_double. f_equiv. mul_permut. + rewrite IHP'. f_equiv. mul_permut. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory