proposition: Lemma Diffble_I_recip : Diffble_I Hab' {1/}G.
proof: Proof. elim diffG; intros G' derG. cut (included I (Dom G)); [ intro Hg' | unfold I, Hab in |- *; Included ]. unfold I in Hg'; cut (forall x : subset I, IMult (IntPartIR Hg') (IntPartIR Hg') x [#] [0]). intro H. exists (IInv (IDiv G' _ H)). eapply Derivative_I_wdr. apply part_int_inv with (F := PartInt (IDiv G' _ H)). apply Feq_reflexive; Included. eapply Derivative_I_wdr. apply Feq_inv with (F := PartInt G'{/}PartInt (IMult (IntPartIR Hg') (IntPartIR Hg'))). apply part_int_div. apply Feq_reflexive; Included. apply Feq_reflexive; simpl in |- *; Included. red in |- *; intros. split. simpl in |- *; Included. elim Gbnd; intros Hinc c. elim c; clear c; intros c H0 H1. exists (c[*]c). apply mult_resp_pos; assumption. intros. simpl in |- *. eapply leEq_wdr. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply mult_resp_leEq_both; auto; apply less_leEq; assumption. eapply Derivative_I_wdr. apply Feq_inv with (F := PartInt G'{/}G{*}G). apply Feq_div. Included. apply Feq_reflexive; Included. apply part_int_mult. FEQ. FEQ. Deriv. intro x. simpl in |- *. apply mult_resp_ap_zero; apply bnd_imp_ap_zero with I; auto; apply scs_prf. Qed.
imports: CoRN.ftc.PartInterval CoRN.ftc.DerivativeOps