fact: Fixpoint Psatz_Q2Z (l : seq positive) (p : Psatz Q) : Psatz Z * positive := match p with | PsatzC (Qmake n d) => (PsatzC n, d) | PsatzLet p1 p2 => let (p1, n1) := Psatz_Q2Z l p1 in let (p2, n2) := Psatz_Q2Z (n1 :: l) p2 in (PsatzLet p1 p2, n2) | PsatzIn n => (PsatzIn _ n, nth 1%positive l n) | PsatzSquare p => let (p, n) := Pol_Q2Z p in (PsatzSquare p, Pos.mul n n) | PsatzMulC p1 p2 => let (p1, n1) := Pol_Q2Z p1 in let (p2, n2) := Psatz_Q2Z l p2 in (PsatzMulC p1 p2, Pos.mul n1 n2) | PsatzMulE p1 p2 => let (p1, n1) := Psatz_Q2Z l p1 in let (p2, n2) := Psatz_Q2Z l p2 in (PsatzMulE p1 p2, Pos.mul n1 n2) | PsatzAdd p1 p2 => let (p1, n1) := Psatz_Q2Z l p1 in let (p2, n2) := Psatz_Q2Z l p2 in let mulc c p := PsatzMulE (PsatzC (Zpos c)) p in (PsatzAdd (mulc n2 p1) (mulc n1 p2), Pos.mul n1 n2) | PsatzZ => (PsatzZ _, 1%positive) 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)