proposition: Lemma lem11a : forall i s k, size s > 1 -> k < size s -> i <= k -> \big[cr_mult/(One:K)]_(x_i <- take (S k) s) (cpoly_linear K [--]x_i (cpoly_one K)) ! (nth Zero s i) [=] Zero.
proof: Proof. intros. rewrite (@eq_big_idx_seq K (@st_eq K) eqv_K (cr_mult) (One:K) morph_K_mult right_unit_K_mult (One:K) K (take (S k) s) _ (fun x : K => (cpoly_linear K [--]x (cpoly_one K)) ! (nth Zero s i)) right_unit_K_mult). assert (take (S k) s = (take i s) ++ ((nth Zero s i) :: (take (k - i) (drop (i + 1) s)))). apply take_nth_drop. omega. exact H0. rewrite H2. rewrite (@big_cat K (@st_eq K) eqv_K cr_mult (One:K) morph_K_mult assoc_K_mult left_unit_K_mult K (take i s) (nth Zero s i :: take (k - i) (drop (i + 1) s)) (fun x : K => true)). rewrite big_cons. assert ((cpoly_linear K [--](nth Zero s i) (cpoly_one K)) ! (nth Zero s i) [=] Zero). simpl. rewrite cring_mult_zero. rewrite cm_rht_unit_unfolded. rewrite mult_one. rewrite cg_lft_inv_unfolded. reflexivity. rewrite H3. rewrite mult_assoc. rewrite cring_mult_zero. rewrite mult_commutes. rewrite cring_mult_zero. reflexivity. destruct s. inversion H. simpl; auto. Qed.
imports: ssreflect CSetoids CSetoidFun CFields CPolynomials Program Omega Equivalence Morphisms Wf Morphisms CRings CRing_Homomorphisms Rational Setoid CPoly_NthCoeff CPoly_Degree CReals Intervals CauchySeq IntervalFunct MoreIntervals MoreFunctions Composition seq bigopsClass