fact: Fixpoint PExpr_Q2Z (e : PExpr Q) : option (PExpr Z) := match e with | PEc (Qmake z 1) => Some (PEc z) | PEc _ => None | PEX n => Some (PEX n) | PEadd e1 e2 => omap2 PEadd (PExpr_Q2Z e1) (PExpr_Q2Z e2) | PEsub e1 e2 => omap2 PEsub (PExpr_Q2Z e1) (PExpr_Q2Z e2) | PEmul e1 e2 => omap2 PEmul (PExpr_Q2Z e1) (PExpr_Q2Z e2) | PEopp e1 => omap PEopp (PExpr_Q2Z e1) | PEpow e1 n => omap (PEpow ^~ n) (PExpr_Q2Z e1) end.
imports: elpi(elpi) Coq(QArith Ring) Coq.micromega(RingMicromega QMicromega EnvRing Tauto Lqa) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify) mathcomp.algebra_tactics(common)