proposition: Lemma default_isIn_ok e1 e2 p1 p2 : match default_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. unfold default_isIn. case PExpr_eq_spec; trivial. intros EQ. rewrite Z.pos_sub_spec. case Pos.compare_spec;intros H; split; try reflexivity. - simpl. now rewrite PE_1_r, H, EQ. - rewrite NPEpow_ok, EQ, <- PEpow_add_r. f_equiv. simpl. f_equiv. now rewrite Pos.add_comm, Pos.sub_add. - simpl. rewrite PE_1_r, EQ. f_equiv. rewrite Z.pos_sub_gt by now apply Pos.sub_decr. simpl. f_equiv. rewrite Pos.sub_sub_distr, Pos.add_comm; trivial. + rewrite Pos.add_sub; trivial. + apply Pos.sub_decr; trivial. - simpl. now apply Z.lt_gt, Pos.sub_decr. Qed.
imports: ZArith_base