proposition: Lemma Continuous_I_inv : Continuous_I Hab {--}F.
proof: Proof. clear incF. elim contF; intros incF' contF'. split. Included. intros e H. elim (contF' e H). intros d H0 H1. exists d. assumption. intros; simpl in |- *. apply leEq_wdl with (AbsIR (F x Hx[-]F y Hy)). apply H1; assumption. eapply eq_transitive_unfolded. apply AbsIR_inv. apply AbsIR_wd; rational. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac