fact: Definition default_isIn e1 p1 e2 p2 := if PExpr_eq e1 e2 then match Z.pos_sub p1 p2 with | Zpos p => Some (Npos p, 1%poly) | Z0 => Some (N0, 1%poly) | Zneg p => Some (N0, e2 ^^ Npos p) end else None.
imports: ZArith_base