proposition: Lemma log_defn_lemma : Continuous (openl [0]) {1/}FId.
proof: Proof. apply Continuous_recip. apply Continuous_id. intros a b Hab H. split. Included. assert (H0 : [0] [<] a). apply H; apply compact_inc_lft. exists a. auto. intros y Hy H1; inversion_clear H1. apply leEq_transitive with y. auto. apply leEq_AbsIR. Qed.
imports: CoRN.ftc.FTC