proposition: Lemma Continuous_I_comp : Continuous_I Hab (G[o]F).
proof: Proof. red in |- *. elim contF; intros incF contF'. elim contG; intros incG contG'. split. exact (included_comp F G a b Hab c d Hcd incF incG Hmap). intros e H. elim (contG' e H). intros dh H0 H1. elim (contF' dh H0). intros df H2 H3. exists df. assumption. intros x y H4 H5 Hx Hy H6. simpl in |- *. cut (forall x : IR, Compact Hab x -> forall Hx, Compact Hcd (F x Hx)). intro H7. apply leEq_wdl with (AbsIR (G _ (incG _ (H7 x H4 (incF x H4))) [-] G _ (incG _ (H7 y H5 (incF y H5))))). apply H1; simpl in |- *. apply H7; assumption. apply H7; assumption. apply H3; assumption. apply AbsIR_wd; rational. intros. apply maps_lemma with G a b Hab; simpl in |- *; assumption. Qed.
imports: CoRN.ftc.MoreFunctions CoRN.ftc.MoreFunSeries