proposition: Theorem isIn_ok e1 p1 e2 p2 : match isIn e1 p1 e2 p2 with | Some(n, e3) => let n' := ZtoN (Zpos p1 - NtoZ n) in (e2 ^ N.pos p2 === e1 ^ n' * e3)%poly /\ (Zpos p1 > NtoZ n)%Z | _ => True end.
proof: Proof. Opaque NPEpow. revert p1 p2. induction e2 as [| |?|?|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe2_1 ? IHe2_2|? IHe|? IHe2 n]; intros p1 p2; try refine (default_isIn_ok e1 _ p1 p2); simpl isIn. - specialize (IHe2_1 p1 p2). destruct isIn as [([|p],e)|]. + split; [|reflexivity]. clear IHe2_2. destruct IHe2_1 as (IH,_). npe_simpl. rewrite IH. npe_ring. + specialize (IHe2_2 p p2). destruct isIn as [([|p'],e')|]. * destruct IHe2_1 as (IH1,GT1). destruct IHe2_2 as (IH2,GT2). split; [|simpl; apply Zgt_trans with (Z.pos p); trivial]. npe_simpl. rewrite IH1, IH2. simpl. simpl_pos_sub. simpl. replace (N.pos p1) with (N.pos p + N.pos (p1 - p))%N. { rewrite PEpow_add_r; npe_ring. } { simpl. f_equal. rewrite Pos.add_comm, Pos.sub_add. - trivial. - now apply Pos.gt_lt. } * destruct IHe2_1 as (IH1,GT1). destruct IHe2_2 as (IH2,GT2). assert (Z.pos p1 > Z.pos p')%Z by (now apply Zgt_trans with (Zpos p)). split; [|simpl; trivial]. npe_simpl. rewrite IH1, IH2. simpl. simpl_pos_sub. simpl. replace (N.pos (p1 - p')) with (N.pos (p1 - p) + N.pos (p - p'))%N. { rewrite PEpow_add_r; npe_ring. } { simpl. f_equal. rewrite Pos.add_sub_assoc, Pos.sub_add; trivial. - now apply Pos.gt_lt. - now apply Pos.gt_lt. } * destruct IHe2_1 as (IH,GT). split; trivial. npe_simpl. rewrite IH. npe_ring. + specialize (IHe2_2 p1 p2). destruct isIn as [(n,e)|]; trivial. destruct IHe2_2 as (IH,GT). split; trivial. set (d := ZtoN (Z.pos p1 - NtoZ n)) in *; clearbody d. npe_simpl. rewrite IH. npe_ring. - destruct n as [|p]; trivial. specialize (IHe2 p1 (p * p2)%positive). destruct isIn as [(n,e)|]; trivial. destruct IHe2 as (IH,GT). split; trivial. set (d := ZtoN (Z.pos p1 - NtoZ n)) in *; clearbody d. now rewrite <- PEpow_mul_r. Qed.
imports: ZArith_base