fact: Definition nformula_of_cutting_plane (t : PolC Z * Z * Op1) : NFormula Z := let (e_z, o) := t in let (e,z) := e_z in (padd e (Pc z) , o).
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory