fact: Definition valid_cut_sign (op:Op1) := match op with | Equal => true | NonStrict => true | _ => false end.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory