fact: Definition ps_monom {α} {r : ring α} (c : α) pow := {| ps_terms := {| terms i := if zerop i then c else 0%K |}; ps_ordnum := Qnum pow; ps_polydo := Qden pow |}.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series