proposition: Lemma cor12 : forall (k : nat) (s : seq K) (Q : fresh_seq K s), k < size s -> nth_coeff k (N K f s k Q) [=] alpha K f s Q k.
proof: Proof. intros. unfold N. cut (mkseq ssrfun.id (k + 1) = mkseq ssrfun.id k ++ [:: k]). intro. rewrite H0. rewrite (@big_cat (cpoly K) (cpoly_eq K) eqv_cpoly (cpoly_plus_cs K) (cpoly_zero K) morph_cpoly assoc_cpoly left_unit_cpoly). rewrite (@big_seq1 (cpoly K) (cpoly_eq K) eqv_cpoly (cpoly_plus_cs K) (cpoly_zero K) right_unit_cpoly). rewrite nth_coeff_plus. rewrite nth_coeff_c_mult_p. assert (nth_coeff k (eta K s k) [=] One). unfold eta. clear H0. induction k. rewrite take0. simpl; reflexivity. cut (take (S k) s = take k s ++ [:: nth Zero s k]). intro. rewrite H0. rewrite (@big_cat (cpoly K) (cpoly_eq K) eqv_cpoly (cpoly_mult_cs K) (cpoly_one K) morph_cpoly_mult assoc_cpoly_mult left_unit_cpoly_mult). rewrite (@big_seq1 (cpoly K) (cpoly_eq K) eqv_cpoly (cpoly_mult_cs K) (cpoly_one K) right_unit_cpoly_mult). rewrite cpoly_mult_lin. rewrite nth_coeff_plus. rewrite coeff_Sm_lin. rewrite cpoly_mult_one. rewrite IHk. unfold cpoly_mult_cr_cs. rewrite cpoly_mult_cr_c_. rewrite nth_coeff_p_mult_c_. assert (degree_le k (\big[cpoly_mult_cs K/cpoly_one K]_(i <- take k s) cpoly_linear K (cg_inv i) (cpoly_one K))). clear IHk H0. induction k. rewrite take0. unfold degree_le. intros. rewrite big_nil. destruct m. inversion H0. simpl; reflexivity. cut (take (S k) s = take k s ++ [:: nth Zero s k]). intro. rewrite H0. unfold degree_le. intros. rewrite (@big_cat (cpoly K) (cpoly_eq K) eqv_cpoly (cpoly_mult_cs K) (cpoly_one K) morph_cpoly_mult assoc_cpoly_mult left_unit_cpoly_mult). set degree_mult_aux. simpl in s0. destruct m. inversion H1. replace (S m) with (m + 1) by omega. rewrite <- cpoly_mult_fast_equiv. rewrite s0. simpl. rewrite mult_one. rewrite cm_rht_unit_unfolded. rewrite mult_one. unfold degree_le in IHk. rewrite IHk. reflexivity. omega. omega. unfold degree_le in IHk. unfold degree_le. intros. rewrite IHk. reflexivity. omega. omega. unfold degree_le. intros. destruct m0. inversion H2. destruct m0. inversion H2. inversion H4. simpl. reflexivity. rewrite cats1. rewrite <- take_nth. reflexivity. apply (ssrbool.introT (P := S k <= size s)). apply ssrnat.leP. omega. unfold degree_le in H1. rewrite H1. rewrite mult_commutes. rewrite cring_mult_zero. algebra. omega. omega. rewrite cats1. rewrite <- take_nth. reflexivity. apply (ssrbool.introT (P := S k <= size s)). apply ssrnat.leP. omega. rewrite H1. rewrite mult_one. assert (degree_le (k - 1) (\big[cpoly_plus_cs K/cpoly_zero K]_(i <- mkseq ssrfun.id k) cr_mult (_C_ (alpha K f s Q i)) (eta K s i))). unfold degree_le. clear H0 H1. induction k. simpl. intros. reflexivity. intros. cut (mkseq ssrfun.id (S k) = mkseq ssrfun.id k ++ [:: k]). intro. rewrite H1. rewrite (@big_cat (cpoly K) (cpoly_eq K) eqv_cpoly (cpoly_plus_cs K) (cpoly_zero K) morph_cpoly assoc_cpoly left_unit_cpoly). rewrite (@big_seq1 (cpoly K) (cpoly_eq K) eqv_cpoly (cpoly_plus_cs K) (cpoly_zero K) right_unit_cpoly). rewrite nth_coeff_plus. unfold degree_le in IHk. rewrite IHk. rewrite cm_lft_unit_unfolded. rewrite nth_coeff_c_mult_p. clear IHk. assert (degree_le k (eta K s k)). unfold degree_le. induction k. unfold degree_le, eta. intros. rewrite take0. destruct m0. assert (1 < 0) by omega. inversion H2. simpl; reflexivity. unfold degree_le, eta. intros. cut (take (S k) s = take k s ++ [:: nth Zero s k]). intro. rewrite H3. rewrite (@big_cat (cpoly K) (cpoly_eq K) eqv_cpoly (cpoly_mult_cs K) (cpoly_one K) morph_cpoly_mult assoc_cpoly_mult left_unit_cpoly_mult). set degree_mult_aux. simpl in s0. rewrite <- cpoly_mult_fast_equiv. destruct m0. inversion H2. replace (S m0) with (m0 + 1) by omega. rewrite s0. unfold degree_le in IHk. rewrite IHk. rewrite mult_commutes. rewrite cring_mult_zero. reflexivity. omega. omega. unfold mkseq. assert ([:: k] = map ssrfun.id (iota k 1)). simpl; reflexivity. rewrite H4. rewrite <- map_cat. rewrite <- iota_add. rewrite ssrnat.addn1. reflexivity. omega. unfold degree_le. intros. rewrite IHk. reflexivity. omega. omega. unfold mkseq. assert ([:: k] = map ssrfun.id (iota k 1)). simpl; reflexivity. rewrite H5. rewrite <- map_cat. rewrite <- iota_add. rewrite ssrnat.addn1. reflexivity. omega. unfold degree_le. intros. simpl. destruct m1. inversion H4. destruct m1. inversion H4. inversion H6. reflexivity. rewrite cats1. rewrite <- take_nth. reflexivity. apply (ssrbool.introT (P := S k <= size s)). apply ssrnat.leP. omega. unfold degree_le in H2. rewrite H2. rewrite cring_mult_zero. reflexivity. omega. omega. omega. unfold mkseq. assert ([:: k] = map ssrfun.id (iota k 1)). simpl; reflexivity. rewrite H1. rewrite <- map_cat. rewrite <- iota_add. rewrite ssrnat.addn1. reflexivity. destruct k. simpl. rewrite cm_lft_unit_unfolded. reflexivity. unfold degree_le in H2. rewrite H2. rewrite cm_lft_unit_unfolded. reflexivity. omega. unfold mkseq. assert ([:: k] = map ssrfun.id (iota k 1)). simpl; reflexivity. rewrite H0. rewrite <- map_cat. rewrite <- iota_add. rewrite ssrnat.addn1. replace (S k) with (k + 1) by omega. reflexivity. 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