proposition: Lemma lem18 : is_derivation C_inf_ab_ralgebra deriv_I_C_inf.
proof: Proof. unfold is_derivation. split. intros. unfold C_inf_ab_eq. apply insq. unfold C_inf_ab_plus. destruct a0. destruct b0. assert (forall x y, f_crr (Build_C_inf_ab x y) = x). intros. auto. rewrite H. assert (f_crr (deriv_I_C_inf (Build_C_inf_ab f_crr0 f_pdf0)) = n_deriv_I a b Hab 1 f_crr0 (f_pdf0 1)). auto. rewrite H0. assert (f_crr (deriv_I_C_inf (Build_C_inf_ab f_crr1 f_pdf1)) = n_deriv_I a b Hab 1 f_crr1 (f_pdf1 1)). auto. rewrite H1. assert (f_crr (deriv_I_C_inf (Build_C_inf_ab (f_crr (Build_C_inf_ab f_crr0 f_pdf0){+} f_crr (Build_C_inf_ab f_crr1 f_pdf1)) (C_inf_ab_plus_obligation_1 (Build_C_inf_ab f_crr0 f_pdf0) (Build_C_inf_ab f_crr1 f_pdf1)))) = n_deriv_I a b Hab 1 (f_crr0{+}f_crr1) (C_inf_ab_plus_obligation_1 (Build_C_inf_ab f_crr0 f_pdf0) (Build_C_inf_ab f_crr1 f_pdf1) 1)). auto. rewrite H2. clear H H0 H1 H2. apply Feq_transitive with (n_deriv_I a b Hab 1 (f_crr0{+}f_crr1) (Diffble_I_n_plus 1 f_crr0 f_crr1 (f_pdf0 1) (f_pdf1 1))). assert ({f_crr0' : CSetoid_fun (subset (Compact (less_leEq _ _ _ Hab))) IR | Derivative_I_n Hab 1 f_crr0 (PartInt f_crr0')}). apply Diffble_I_n_imp_deriv_n. apply f_pdf0. inversion_clear X. assert (Derivative_I_n Hab 1 f_crr0 (n_deriv_I a b Hab 1 f_crr0 (f_pdf0 1))). apply n_deriv_lemma. assert (Feq (Compact (less_leEq IR a b Hab)) (PartInt x) (n_deriv_I a b Hab 1 f_crr0 (f_pdf0 1))). apply (Derivative_I_n_unique a b Hab 1 f_crr0). exact X0. exact X. assert ({f_crr1' : CSetoid_fun (subset (Compact (less_leEq _ _ _ Hab))) IR | Derivative_I_n Hab 1 f_crr1 (PartInt f_crr1')}). apply Diffble_I_n_imp_deriv_n. apply f_pdf1. inversion_clear X2. assert (Derivative_I_n Hab 1 f_crr1 (n_deriv_I a b Hab 1 f_crr1 (f_pdf1 1))). apply n_deriv_lemma. assert (Feq (Compact (less_leEq IR a b Hab)) (PartInt x0) (n_deriv_I a b Hab 1 f_crr1 (f_pdf1 1))). apply (Derivative_I_n_unique a b Hab 1 f_crr1). exact X3. exact X2. assert (Feq (Compact (less_leEq IR a b Hab)) (PartInt x{+}PartInt x0) ((n_deriv_I a b Hab 1 f_crr0 (f_pdf0 1)){+} (n_deriv_I a b Hab 1 f_crr1 (f_pdf1 1)))). apply Feq_plus. exact X1. exact X4. apply Feq_transitive with (PartInt x{+}PartInt x0). apply Feq_plus. apply Feq_symmetric; exact X1. apply Feq_symmetric; exact X4. assert (Derivative_I_n Hab 1 (f_crr0{+}f_crr1) (PartInt x{+}PartInt x0)). apply Derivative_I_n_add. exact X0. exact X3. assert (Derivative_I_n Hab 1 (f_crr0{+}f_crr1) ((n_deriv_I a b Hab 1 (f_crr0{+}f_crr1) (Diffble_I_n_plus 1 f_crr0 f_crr1 (f_pdf0 1) (f_pdf1 1))))). apply n_deriv_lemma. apply (Derivative_I_n_unique a b Hab 1 (f_crr0{+}f_crr1)). exact X6. exact X7. apply n_deriv_I_wd. apply Feq_plus. apply Feq_reflexive. apply Diffble_I_n_imp_inc with 42. apply f_pdf0. apply Feq_reflexive. apply Diffble_I_n_imp_inc with 42. apply f_pdf1. split. intros. unfold C_inf_ab_eq. apply insq. unfold C_inf_ab_ralg_act. assert (forall x y, f_crr (Build_C_inf_ab x y) = x) by auto. rewrite H. destruct a0. assert (f_crr (deriv_I_C_inf (Build_C_inf_ab f_crr0 f_pdf0)) = n_deriv_I a b Hab 1 f_crr0 (f_pdf0 1)). auto. rewrite H0. assert ( f_crr (deriv_I_C_inf (Build_C_inf_ab (c{**}f_crr (Build_C_inf_ab f_crr0 f_pdf0)) (C_inf_ab_ralg_act_obligation_1 c (Build_C_inf_ab f_crr0 f_pdf0)))) = n_deriv_I a b Hab 1 (c{**}f_crr0) (C_inf_ab_ralg_act_obligation_1 c (Build_C_inf_ab f_crr0 f_pdf0) 1)). auto. rewrite H1. clear H H0 H1. apply Feq_transitive with (n_deriv_I a b Hab 1 (c{**}f_crr0) (Diffble_I_n_cmul 1 f_crr0 c (f_pdf0 1))). assert ({f_crr0' : CSetoid_fun (subset (Compact (less_leEq _ _ _ Hab))) IR | Derivative_I_n Hab 1 f_crr0 (PartInt f_crr0')}). apply Diffble_I_n_imp_deriv_n. apply f_pdf0. inversion_clear X. assert (Derivative_I_n Hab 1 f_crr0 (n_deriv_I a b Hab 1 f_crr0 (f_pdf0 1))). apply n_deriv_lemma. assert (Feq (Compact (less_leEq IR a b Hab)) (PartInt x) (n_deriv_I a b Hab 1 f_crr0 (f_pdf0 1))). apply (Derivative_I_n_unique a b Hab 1 f_crr0). exact X0. exact X. assert (Derivative_I_n Hab 1 (c{**}f_crr0) (c{**}PartInt x)). apply Derivative_I_n_cmul. exact X0. assert (Derivative_I_n Hab 1 (c{**}f_crr0) ((n_deriv_I a b Hab 1 (c{**}f_crr0) (Diffble_I_n_cmul 1 f_crr0 c (f_pdf0 1))))). apply n_deriv_lemma. apply Feq_transitive with (c{**}PartInt x). unfold Fscalmult. apply Feq_mult. apply Feq_reflexive. unfold included; simpl; auto. apply Feq_symmetric. exact X1. assert (Derivative_I_n Hab 1 (c{**}f_crr0) (c{**}(n_deriv_I a b Hab 1 f_crr0 (f_pdf0 1)))). apply Derivative_I_n_cmul. apply n_deriv_lemma. assert (Derivative_I_n Hab 1 (c{**}f_crr0) (c{**}PartInt x)). apply Derivative_I_n_cmul. exact X0. apply Feq_transitive with (c{**}n_deriv_I a b Hab 1 f_crr0 (f_pdf0 1)). unfold Fscalmult. apply Feq_mult. apply Feq_reflexive. unfold included; simpl; auto. exact X1. apply Feq_transitive with (c{**}PartInt x). apply (Derivative_I_n_unique a b Hab 1 (c{**}f_crr0)). exact X4. exact X2. apply Feq_transitive with (c{**}n_deriv_I a b Hab 1 f_crr0 (f_pdf0 1)). unfold Fscalmult. apply Feq_mult. apply Feq_reflexive. unfold included; simpl; auto. exact X1. apply (Derivative_I_n_unique a b Hab 1 (c{**}f_crr0)). exact X4. exact X3. apply n_deriv_I_wd. unfold Fscalmult. apply Feq_mult. apply Feq_reflexive. unfold included; simpl; auto. apply Feq_reflexive. apply Diffble_I_n_imp_inc with 42. apply f_pdf0. intros. unfold C_inf_ab_eq. apply insq. destruct a0. destruct b0. unfold C_inf_ab_mult, C_inf_ab_plus. set (f_crr (Build_C_inf_ab f_crr0 f_pdf0)). set (f_crr (Build_C_inf_ab f_crr1 f_pdf1)). set (deriv_I_C_inf (Build_C_inf_ab f_crr0 f_pdf0)). set (deriv_I_C_inf (Build_C_inf_ab f_crr1 f_pdf1)). set (Build_C_inf_ab f_crr0 f_pdf0). set (Build_C_inf_ab f_crr1 f_pdf1). replace (f_crr (deriv_I_C_inf (Build_C_inf_ab (p{*}p0) (C_inf_ab_mult_obligation_1 c1 c2)))) with (n_deriv_I a b Hab 1 (p{*}p0) (C_inf_ab_mult_obligation_1 c1 c2 1)) by auto. replace (f_crr (Build_C_inf_ab (f_crr (Build_C_inf_ab (p{*}f_crr c0) (C_inf_ab_mult_obligation_1 c1 c0)){+} f_crr (Build_C_inf_ab (f_crr c{*}p0) (C_inf_ab_mult_obligation_1 c c2))) (C_inf_ab_plus_obligation_1 (Build_C_inf_ab (p{*}f_crr c0) (C_inf_ab_mult_obligation_1 c1 c0)) (Build_C_inf_ab (f_crr c{*}p0) (C_inf_ab_mult_obligation_1 c c2))))) with (f_crr (Build_C_inf_ab (p{*}f_crr c0) (C_inf_ab_mult_obligation_1 c1 c0)){+} f_crr (Build_C_inf_ab (f_crr c{*}p0) (C_inf_ab_mult_obligation_1 c c2))) by auto. replace (f_crr ((Build_C_inf_ab (f_crr c{*}p0) (C_inf_ab_mult_obligation_1 c c2)))) with (f_crr c{*}p0) by auto. replace (f_crr (Build_C_inf_ab (p{*}f_crr c0) (C_inf_ab_mult_obligation_1 c1 c0))) with (p{*}f_crr c0) by auto. assert (Derivative_I_n Hab 1 (p{*}p0) (n_deriv_I a b Hab 1 (p{*}p0) (C_inf_ab_mult_obligation_1 c1 c2 1))). apply n_deriv_lemma. assert ({f_crr0' : CSetoid_fun (subset (Compact (less_leEq _ _ _ Hab))) IR | Derivative_I_n Hab 1 f_crr0 (PartInt f_crr0')}). apply Diffble_I_n_imp_deriv_n. apply f_pdf0. inversion_clear X0. assert ({f_crr1' : CSetoid_fun (subset (Compact (less_leEq _ _ _ Hab))) IR | Derivative_I_n Hab 1 f_crr1 (PartInt f_crr1')}). apply Diffble_I_n_imp_deriv_n. apply f_pdf1. inversion_clear X0. assert (Derivative_I_n Hab 1 (p{*}p0) (f_crr0{*}PartInt x0{+}PartInt x{*}f_crr1)). simpl. assert (included (Compact (less_leEq _ _ _ Hab)) (Dom (f_crr0{*}PartInt x0{+}PartInt x{*}f_crr1))). apply included_FPlus. apply included_FMult. apply (Derivative_I_n_imp_inc a b Hab 1 f_crr0 (PartInt x)). exact X1. apply (Derivative_I_n_imp_inc' a b Hab 1 f_crr1 (PartInt x0)). exact X2. apply included_FMult. apply (Derivative_I_n_imp_inc' a b Hab 1 f_crr0 (PartInt x)). exact X1. apply (Derivative_I_n_imp_inc a b Hab 1 f_crr1 (PartInt x0)). exact X2. exists (@IntPartIR (f_crr0{*}PartInt x0{+}PartInt x{*}f_crr1) a b (less_leEq _ _ _ Hab) X0). apply Derivative_I_wdr with (f_crr0{*}PartInt x0{+}PartInt x{*}f_crr1). apply int_part_int. replace p with f_crr0 by auto. replace p0 with f_crr1 by auto. apply Derivative_I_mult. simpl in X1. inversion_clear X1. apply Derivative_I_wdr with (PartInt x1). exact X4. exact X3. simpl in X2. inversion_clear X2. apply Derivative_I_wdr with (PartInt x1). exact X4. exact X3. apply Feq_symmetric. apply int_part_int. apply Feq_transitive with (p{*}f_crr c0{+}f_crr c{*}p0). apply (Derivative_I_n_unique a b Hab 1 (p{*}p0)). exact X. replace p with f_crr0 by auto. replace p0 with f_crr1 by auto. replace (f_crr c0) with (n_deriv_I a b Hab 1 f_crr1 (f_pdf1 1)) by auto. replace (f_crr c) with (n_deriv_I a b Hab 1 f_crr0 (f_pdf0 1)) by auto. replace p with f_crr0 in X0 by auto. replace p0 with f_crr1 in X0 by auto. apply Derivative_I_n_wdr with (f_crr0{*}PartInt x0{+}PartInt x{*}f_crr1). apply Feq_plus. apply Feq_mult. apply Feq_reflexive. apply (Derivative_I_n_imp_inc a b Hab 1 f_crr0 (PartInt x)). exact X1. assert (Derivative_I_n Hab 1 f_crr1 (n_deriv_I a b Hab 1 f_crr1 (f_pdf1 1))). apply n_deriv_lemma. apply (Derivative_I_n_unique a b Hab 1 f_crr1). exact X2. apply n_deriv_lemma. apply Feq_mult. apply (Derivative_I_n_unique a b Hab 1 f_crr0). exact X1. apply n_deriv_lemma. apply Feq_reflexive. apply (Derivative_I_n_imp_inc a b Hab 1 f_crr1 (PartInt x0)). exact X2. exact X0. apply Feq_reflexive. apply included_FPlus. apply included_FMult. replace p with f_crr0 by auto. apply (Derivative_I_n_imp_inc a b Hab 1 f_crr0 (PartInt x)). exact X1. replace (f_crr c0) with (n_deriv_I a b Hab 1 f_crr1 (f_pdf1 1)) by auto. apply n_deriv_inc. apply included_FMult. replace (f_crr c) with (n_deriv_I a b Hab 1 f_crr0 (f_pdf0 1)) by auto. apply n_deriv_inc. replace p0 with f_crr1 by auto. apply (Derivative_I_n_imp_inc a b Hab 1 f_crr1 (PartInt x0)). exact X2. 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