proposition: Lemma Rinv_continuous (x : R) : x <> 0 -> @continuous_at RTop RTop Rinv x.
proof: Proof. intros. apply continuous_at_iff_continuity_pt, continuity_pt_inv; trivial. apply derivable_continuous_pt, derivable_pt_id. Qed.
imports: RTopology ProductTopology Homeomorphisms ContinuousFactorization Coq(FunctionalExtensionality Lra ProofIrrelevance) ZornsLemma(EnsembleProduct EnsemblesTactics)