proposition: Lemma lem11 : forall (k i : nat) (s : seq K) (P : i <= k) (Q : fresh_seq K s), k < size s -> f (nth Zero s i) [=] (N K f s k Q) ! (nth Zero s i).
proof: Proof. intros. induction k. inversion P. destruct s. inversion H. simpl. unfold alpha. assert (fresh_seq K [:: s]). apply fresh_cons. unfold sqfresh. apply insq. simpl; auto. apply fresh_nil. assert (dd K f (rev (take (0 + 1) (s :: s0))) (rev_fresh_seq K (take (0 + 1) (s :: s0)) (take_fresh_seq K (0 + 1) (s :: s0) Q)) [=] dd K f [:: s] H1). apply dd_indep. simpl. rewrite take0. reflexivity. rewrite H2. assert (f s [=] dd K f [:: s] H1). algebra. rewrite <- H3. rewrite cring_mult_zero. rewrite cm_rht_unit_unfolded. rewrite cm_rht_unit_unfolded. algebra. inversion P. assert (fresh_seq K (nth Zero s (S k) :: rev (take (S k - S k) s))). assert (S k - S k = 0) by omega. rewrite H1. rewrite take0. apply fresh_cons. unfold sqfresh. apply insq. simpl; auto. apply rev_fresh_seq. apply fresh_nil. rewrite (lem11b (S k) (S k) _ _ H1). assert (mkseq ssrfun.id (S k - S k) = Nil nat). assert (S k - S k = 0) by omega. rewrite H2. auto. rewrite H2. rewrite big_nil. assert (fresh_seq K [:: nth Zero s (S k)]). apply fresh_cons. unfold sqfresh. apply insq. simpl; auto. apply fresh_nil. setoid_replace (dd K f (nth Zero s (S k) :: (rev (take (S k - S k) s))) H1) with (dd K f [:: nth Zero s (S k)] H3). assert (cpoly_apply_fun (cpoly_zero K) (nth Zero s (S k)) [=] Zero). algebra. rewrite H4. rewrite cm_lft_unit_unfolded. unfold eta. assert (take (S k - S k) s = Nil K). assert (S k - S k = 0) by omega. rewrite H5. rewrite take0; reflexivity. rewrite H5. rewrite apply_bigops. rewrite big_nil. rewrite mult_one. algebra. apply dd_indep. assert (S k - S k = 0) by omega. rewrite H4. rewrite take0. auto. omega. auto. omega. unfold N. rewrite (@eq_big_idx_seq (cpoly K) (cpoly_eq K) eqv_cpoly (cpoly_plus_cs K) (cpoly_zero K) morph_cpoly right_unit_cpoly (cpoly_zero K) nat (mkseq ssrfun.id (S k + 1)) (fun x : nat => true) (fun x : nat => cr_mult (_C_ (alpha K f s Q x)) (eta K s x)) right_unit_cpoly). assert (mkseq ssrfun.id (S (k + 1)) = (mkseq ssrfun.id (S k)) ++ [:: S k]). unfold mkseq. replace (S (S k)) with (S k + 1). rewrite (iota_add 0 (S k) 1). rewrite map_cat; auto. omega. rewrite H2. clear H2. 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 (S k)) ([:: S k]) (fun x : nat => true) (fun x : nat => _C_ (alpha K f s Q x) [*] (eta K s x))). unfold N in IHk. rewrite (@big_seq1 (cpoly K) (cpoly_eq K) eqv_cpoly (cpoly_plus_cs K) (cpoly_zero K) right_unit_cpoly nat (S k) (fun x : nat => _C_ (alpha K f s Q x) [*] (eta K s x))). rewrite (@plus_apply K ((\big[cpoly_plus_cs K/cpoly_zero K]_(i0 <- mkseq ssrfun.id (S k)) (_C_ (alpha K f s Q i0) [*] (eta K s i0)))) (_C_ (alpha K f s Q (S k)) [*] (eta K s (S k))) (nth Zero s i)). assert ((_C_ (alpha K f s Q (S k)) [*] (eta K s (S k))) ! (nth Zero s i) [=] Zero). rewrite c_mult_apply. unfold eta. rewrite (@apply_bigops (take (S k) s)). rewrite lem11a. rewrite cring_mult_zero. reflexivity. omega. omega. exact H1. rewrite H2. rewrite IHk. assert (S k = k + 1) by omega. rewrite H3. rewrite cm_rht_unit_unfolded. reflexivity. exact H1. omega. 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