proposition: Theorem split_aux_ok: forall e1 p e2, (e1 ^ Npos p === left (split_aux e1 p e2) * common (split_aux e1 p e2) /\ e2 === right (split_aux e1 p e2) * common (split_aux e1 p e2))%poly.
proof: Proof. intro e1;induction e1 as [| |?|?|? IHe1_1 ? IHe1_2|? IHe1_1 ? IHe1_2|e1_1 IHe1_1 ? IHe1_2|? IHe1|? IHe1 n]; intros k e2; try refine (split_aux_ok1 _ k e2);simpl. - destruct (IHe1_1 k e2) as (H1,H2). destruct (IHe1_2 k (right (split_aux e1_1 k e2))) as (H3,H4). clear IHe1_1 IHe1_2. npe_simpl; split. + rewrite H1, H3. npe_ring. + rewrite H2 at 1. rewrite H4 at 1. npe_ring. - destruct n; simpl. + rewrite PEpow_0_r, PEpow_1_l, !PE_1_r. now split. + rewrite <- PEpow_mul_r. simpl. apply IHe1. Qed.
imports: ZArith_base