proposition: Lemma Rdiv_continuous: forall x y:R, y <> 0 -> continuous_at_2arg Rdiv x y (X:=RTop) (Y:=RTop) (Z:=RTop).
proof: Proof. intros. red. match goal with |- continuous_at ?f ?q => replace f with (fun p:point_set RTop * point_set RTop => fst p * / snd p) end. - apply product_continuous. + apply continuous_func_continuous_everywhere; apply product2_fst_continuous. + apply continuous_composition_at. * simpl. now apply Rinv_continuous. * apply continuous_func_continuous_everywhere; apply product2_snd_continuous. - extensionality p. now destruct p. Qed.
imports: RTopology ProductTopology Homeomorphisms ContinuousFactorization Coq(FunctionalExtensionality Lra ProofIrrelevance) ZornsLemma(EnsembleProduct EnsemblesTactics)