fact: Fixpoint toPol (e: Expr V) := match e with | Var v => PX 1 v 0 | Zero => 0 | One => 1 | Plus a b => add (toPol a) (toPol b) | Mult a b => mul (toPol a) (toPol b) | Neg a => mulC (almost_negate 1) (toPol a) end.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.additional_operations HoTT.Classes.tactics.ring_quote HoTT.Classes.theory.rings