proposition: Lemma split_aux_ok1 e1 p e2 : (let res := match isIn e1 p e2 1 with | Some (N0,e3) => mk_rsplit 1 (e1 ^^ Npos p) e3 | Some (Npos q, e3) => mk_rsplit (e1 ^^ Npos q) (e1 ^^ Npos (p - q)) e3 | None => mk_rsplit (e1 ^^ Npos p) 1 e2 end in e1 ^ Npos p === left res * common res /\ e2 === right res * common res)%poly.
proof: Proof. Opaque NPEpow NPEmul. intros res. unfold res;clear res; generalize (isIn_ok e1 p e2 xH). destruct (isIn e1 p e2 1) as [([|p'],e')|]; simpl. - intros (H1,H2); split; npe_simpl. + now rewrite PE_1_l. + rewrite PEpow_1_r in H1. rewrite H1. npe_ring. - intros (H1,H2); split; npe_simpl. + rewrite <- PEpow_add_r. f_equiv. simpl. f_equal. rewrite Pos.add_comm, Pos.sub_add; trivial. now apply Z.gt_lt in H2. + rewrite PEpow_1_r in H1. rewrite H1. simpl_pos_sub. simpl. npe_ring. - intros _; split; npe_simpl; now rewrite PE_1_r. Qed.
imports: ZArith_base