fact: Definition functional (x: Q): CR := Σ (map (fun p => let '((xj, y), rest) := p in y [*] ' Π (map (fun xi => (x - fst xi) * / (xj - fst xi))%Q rest)) (separates qpoints)).
imports: Unicode.Utf8 Setoid Arith List Program Permutation CSetoids CRings CPoly_Degree CPoly_ApZero CRArith Qmetric Qring CReals stdlib_omissions.Pair stdlib_omissions.Q list_separates SetoidPermutation