proposition: Lemma lem11b : forall (k c : nat) (s : seq K) (Q : fresh_seq K s) (R : fresh_seq K ((nth Zero s k) :: (rev (take (k - c) s)))), 0 < k -> c <= k -> k < size s -> (N K f s k Q) ! (nth Zero s k) [=] (\big[(cpoly_plus_cs K)/(cpoly_zero K)]_(j <- (mkseq (fun x => x) (k - c)) | (fun x => true) j) (_C_ (alpha K f s Q j) [*] (eta K s j))) ! (nth Zero s k) [+] (dd K f ((nth Zero s k) :: (rev (take (k - c) s))) R) [*] (eta K s (k - c)) ! (nth Zero s k).
proof: Proof. intros. induction c. assert (k - 0 = k) by omega. assert (mkseq ssrfun.id (k - 0) = mkseq ssrfun.id k). rewrite H2; reflexivity. rewrite H3. clear H2 H3. assert (fresh_seq K (rev (take k s))). apply rev_fresh_seq. apply take_fresh_seq. exact Q. assert (dd K f (nth Zero s k :: rev (take (k - 0) s)) R [=] alpha K f s Q k). unfold alpha. apply dd_indep. rewrite <- cat1s. assert (rev [:: nth Zero s k] = [:: nth Zero s k]). auto. rewrite <- H3. rewrite <- rev_cat. assert (take (k - 0) s ++ [:: nth Zero s k] = take (k + 1) s). rewrite cats1. assert (k - 0 = k) by omega. rewrite H4. rewrite <- take_nth. assert (S k = k + 1) by omega. rewrite H5. reflexivity. apply (ssrbool.introT (P := S k <= size s)). apply ssrnat.leP. auto. rewrite H4. reflexivity. rewrite H3. rewrite <- c_mult_apply. rewrite <- plus_apply. assert (k - 0 = k) by omega. rewrite H4. rewrite <- (@big_seq1 (cpoly K) (cpoly_eq K) eqv_cpoly (cpoly_plus_cs K) (cpoly_zero K) right_unit_cpoly nat k (fun x => cr_mult (_C_ (alpha K f s Q x)) (eta K s x))). rewrite <- (@big_cat (cpoly K) (cpoly_eq K) (eqv_cpoly) (cpoly_plus_cs K) (cpoly_zero K) morph_cpoly assoc_cpoly left_unit_cpoly nat (mkseq ssrfun.id k) ([:: k]) (fun x => true) (fun x => cr_mult (_C_ (alpha K f s Q x)) (eta K s x)) ). simpl. assert (mkseq ssrfun.id k ++ [:: k] = mkseq ssrfun.id (k + 1)). unfold mkseq. assert ([:: k] = map ssrfun.id [:: k]). auto. rewrite H5. rewrite <- map_cat. assert ([:: k] = iota k 1). auto. rewrite H6. rewrite <- iota_add. auto. rewrite H5. reflexivity. assert (fresh_seq K (nth Zero s k :: rev (take (k - c) s))). apply fresh_cons. unfold sqfresh. apply insq. apply rev_fresh. apply nth_fresh. exact H1. exact Q. apply rev_fresh_seq. apply take_fresh_seq. exact Q. rewrite (IHc H2). assert (mkseq ssrfun.id (k - c) = mkseq ssrfun.id (k - S c) ++ [:: (k - S c)]). unfold mkseq. assert ([:: k - S c] = map ssrfun.id (iota (k - S c) 1)) by auto. rewrite H3. rewrite <- map_cat. assert (iota (k - S c) 1 = iota (0 + (k - S c)) 1) by auto. rewrite H4. rewrite <- iota_add. assert (ssrnat.addn (k - S c) 1 = k - c). rewrite ssrnat.addn1. omega. rewrite H5; reflexivity. rewrite H3. rewrite (@big_cat (cpoly K) (cpoly_eq K) eqv_cpoly (cpoly_plus_cs K) (cpoly_zero K) morph_cpoly assoc_cpoly left_unit_cpoly nat (mkseq ssrfun.id (k - S c)) [:: k - S c] ). rewrite plus_apply. set (CSemiGroups.plus_assoc K). unfold associative in a. rewrite <- a. rewrite (@big_seq1 (cpoly K) (cpoly_eq K) eqv_cpoly (cpoly_plus_cs K) (cpoly_zero K) right_unit_cpoly nat (k - S c)). assert (fresh_seq K (rev (take (k - c) s))). apply rev_fresh_seq. apply take_fresh_seq. exact Q. assert ((nth Zero s k) [-] (nth Zero s (k - S c)) [#] Zero). apply ap_fresh_nth. omega. omega. exact H1. exact Q. assert ((dd K f (nth Zero s k :: rev (take (k - c) s)) H2) [=] (((dd K f (nth Zero s k :: rev (take (k - S c) s)) R) [-] (dd K f (rev (take (k - c) s)) H4)) [/] ((nth Zero s k) [-] (nth Zero s (k - S c))) [//] X)). apply dd_reduce_nth. exact H. omega. exact H1. exact Q. rewrite H5. unfold eta at 3. assert (\big[cpoly_mult_cs K/cpoly_one K]_(x_i <- take (k - c) s) (cpoly_linear K (cg_inv x_i) (cpoly_one K)) [=] \big[cpoly_mult_cs K/cpoly_one K]_(x_i <- (take (k - S c) s) ++ [:: nth Zero s (k - S c)]) (cpoly_linear K (cg_inv x_i) (cpoly_one K))). assert (take (k - c) s = take (k - S c) s ++ [:: nth Zero s (k - S c)]). rewrite <- cat_rcons. rewrite <- take_nth. assert (k - c = S (k - S c)) by omega. rewrite H6. rewrite cats0; reflexivity. apply (ssrbool.introT (P := S (k - S c) <= size s)). apply ssrnat.leP. omega. rewrite H6. reflexivity. rewrite H6. 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 K (take (k - S c) s) [:: nth Zero s (k - S c)]). rewrite (@big_seq1 (cpoly K) (cpoly_eq K) eqv_cpoly (cpoly_mult_cs K) (cpoly_one K) right_unit_cpoly_mult K (nth Zero s (k - S c))). rewrite (mult_apply K _ (cpoly_linear K (cg_inv (nth Zero s (k - S c))) (cpoly_one K))). assert (cpoly_apply_fun (cpoly_linear K (cg_inv (nth Zero s (k - S c))) (cpoly_one K)) (nth Zero s k) [=] nth Zero s k [-] nth Zero s (k - S c)). simpl. rewrite cring_mult_zero. rewrite cm_rht_unit_unfolded. rewrite mult_one. rewrite cg_minus_unfolded. algebra. rewrite H7. rewrite (mult_commutes K _ (nth Zero s k [-] nth Zero s (k - S c))). rewrite mult_assoc. rewrite div_1. rewrite (mult_commutes K (_ [-] _) _). rewrite ring_dist_minus. unfold alpha at 2. assert (dd K f (rev (take (k - S c + 1) s)) (rev_fresh_seq K (take (k - S c + 1) s) (take_fresh_seq K (k - S c + 1) s Q)) [=] dd K f (rev (take (k - c) s)) H4). apply dd_indep. assert (k - S c + 1 = k - c) by omega. rewrite H8. reflexivity. rewrite H8. rewrite cg_minus_unfolded. rewrite (cag_commutes K _ (cg_inv _)). rewrite (a _ (cg_inv _)). unfold eta at 2. rewrite c_mult_apply. rewrite (mult_commutes K _ (dd _ _ _ H4)). rewrite cg_rht_inv_unfolded. rewrite cm_lft_unit_unfolded. rewrite (mult_commutes K (dd _ _ _ _) _). unfold eta at 3. reflexivity. omega. 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