proposition: Lemma apply x: (L ! ' x) [=] functional x.
proof: Proof. unfold L, functional. rewrite cm_Sum_apply. autorewrite with apply. rewrite map_map. apply (@cm_Sum_eq _). intros [[u v] w]. autorewrite with apply. apply mult_wd. reflexivity. rewrite inject_Q_product. rewrite cr_Product_apply. do 2 rewrite map_map. apply (@cm_Sum_eq (Build_multCMonoid CRasCRing)). intros [p q]. rewrite <- CRmult_Qmult. autorewrite with apply. change (((' (- p)%Q + ' x * (1 + ' x * 0)) * ' (/ (u - p))) == (' (x + - p)%Q * ' (/ (u - p))))%CR. rewrite <- CRplus_Qplus. generalize (/ (u - p)). intros. ring. Qed.
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