proposition: Lemma Diffble_I_n_div : forall (n : nat) (f g : PartFunct IR) (Pfdf : Diffble_I_n Hab n f) (Pgdf : Diffble_I_n Hab n g) (Pbnd : bnd_away_zero (Compact (less_leEq _ _ _ Hab)) g), Diffble_I_n Hab n (Fdiv f g).
proof: Proof. intro n. induction n. intros f0 g Hf0 Hg Hbnd. simpl. unfold included. intros. red. split. simpl in Hf0. unfold included in Hf0. apply Hf0. exact H. red. split. simpl in Hg. unfold included in Hg. apply Hg. exact H. intros. elim Hbnd. intros. elim b0. intros. apply AbsIR_cancel_ap_zero. apply pos_ap_zero. apply less_leEq_trans with x0. exact p. apply q. exact H. intros. simpl. simpl in Pfdf. inversion Pfdf. inversion x. simpl in Pgdf. inversion Pgdf. inversion x1. assert (Derivative_I Hab (f{/}g) (((PartInt x0){*}g{-}f{*}(PartInt x2)){/} (g{*}g))). apply Derivative_I_div. exact X0. exact X2. exact Pbnd. assert (Diffble_I Hab (f{/}g)). apply deriv_imp_Diffble_I with ((PartInt x0{*}g{-}f{*}PartInt x2){/}g{*}g). exact X3. exists X4. destruct X4. simpl. apply Diffble_I_n_wd with ((PartInt x0{*}g{-}f{*}PartInt x2){/}g{*}g). apply Derivative_I_unique with (f{/}g). exact X3. exact d. apply IHn. apply Diffble_I_n_minus. apply Diffble_I_n_mult. replace n with (pred (S n)) by omega. apply Diffble_I_imp_le with f. omega. simpl. exists x. exact X. exact X0. apply le_imp_Diffble_I with (S n). omega. simpl. exact Pgdf. apply Diffble_I_n_mult. apply le_imp_Diffble_I with (S n). omega. simpl. exact Pfdf. replace n with (pred (S n)) by omega. apply Diffble_I_imp_le with g. omega. simpl. exact Pgdf. exact X2. apply Diffble_I_n_mult. apply le_imp_Diffble_I with (S n). omega. simpl. exact Pgdf. apply le_imp_Diffble_I with (S n). omega. simpl. exact Pgdf. unfold bnd_away_zero. split. apply included_FMult. apply Diffble_I_n_imp_inc with (S n). simpl. exact Pgdf. apply Diffble_I_n_imp_inc with (S n). simpl. exact Pgdf. unfold bnd_away_zero in Pbnd. inversion Pbnd. inversion X5. exists (x4[*]x4). apply mult_resp_pos. exact X6. exact X6. intros. rewrite AbsIR_resp_mult. apply mult_resp_leEq_both. algebra. algebra. apply H. exact H0. apply H. exact H0. 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 Structures