proposition: Lemma dd_reduce : forall (s : seq K) (a b : K) (P1 : fresh_seq K (a :: b :: s)) (P2 : fresh_seq K (a :: s)) (P3 : fresh_seq K (b :: s)) (P4 : a [-] b [#] Zero), (dd K f (a :: b :: s) P1) = (((dd K f (a :: s) P2) [-] (dd K f (b :: s) P3)) [/] (a [-] b) [//] P4).
proof: Proof. intros. Admitted. Lemma dd_reduce_nth : forall (s : seq K) (k c : nat) (P : fresh_seq K (nth Zero s k :: rev (take (k - c) s))) (Q : fresh_seq K (nth Zero s k :: rev (take (k - S c) s))) (R : fresh_seq K (rev (take (k - c) s))) (X : (nth Zero s k) [-] (nth Zero s (k - S c)) [#] Zero), 0 < k -> c < k -> k < size s -> fresh_seq K s -> (dd K f (nth Zero s k :: rev (take (k - c) s)) P) [=] ((dd K f (nth Zero s k :: rev (take (k - S c) s)) Q)[-] (dd K f (rev (take (k - c) s)) R)[/] (nth Zero s k[-]nth Zero s (k - S c))[//]X). Proof. intros. assert (fresh_seq K (nth Zero s k :: nth Zero s (k - S c) :: rev (take (k - S c) s))). apply fresh_cons. unfold sqfresh. apply insq. simpl. split. apply zero_minus_apart. algebra. apply rev_fresh. apply nth_fresh. exact H1. exact H2. apply fresh_cons. unfold sqfresh. apply insq. assert (forall k, k < size s -> fresh K (rev (take k s)) (nth Zero s k)). intros. apply rev_fresh. assert (take k0 s = take (k0 - 0) s). replace (k0 - 0) with k0 by omega; reflexivity. rewrite H4. apply nth_fresh. exact H3. exact H2. apply X0. omega. apply rev_fresh_seq. apply take_fresh_seq. exact H2. assert (rev (take (k - c) s) = nth Zero s (k - S c) :: rev (take (k - S c) s)). assert (k - c = (S (k - S c))) by omega. rewrite H4. set (@take_nth). rewrite (@take_nth K Zero (k - S c) s). rewrite rev_rcons; reflexivity. apply (ssrbool.introT (P := S (k - S c) <= size s)). apply ssrnat.leP. omega. assert ((dd K f (nth Zero s k :: rev (take (k - c) s)) P) [=] (dd K f [:: nth Zero s k, nth Zero s (k - S c) & rev (take (k - S c) s)] H3)). apply dd_indep. rewrite H4; reflexivity. rewrite H5. assert (fresh_seq K ((nth Zero s (k - S c)) :: rev (take (k - S c) s))). inversion H3. exact H9. assert ((dd K f (rev (take (k - c) s)) R) [=] (dd K f (nth Zero s (k - S c) :: rev (take (k - S c) s)) H6)). apply dd_indep. rewrite H4; reflexivity. unfold cf_div. rewrite H7. set (dd_reduce (rev (take (k - S c) s)) (nth Zero s k) (nth Zero s (k - S c)) H3 Q H6 X). unfold cf_div in e. rewrite e. 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