fact: Definition pexpr_times_nformula (e: PolC) (f : NFormula) : option NFormula := let (ef,o) := f in match o with | Equal => Some (Pmul cO cI cplus ctimes ceqb e ef , Equal) | _ => None end.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl