proposition: Lemma continuity_2d_pt_inv (f : R -> R -> R) (x y : R) : continuity_2d_pt f x y -> f x y <> 0 -> continuity_2d_pt (fun u v => / f u v) x y.
proof: Proof. intros Cf Df. apply continuity_2d_pt_filterlim in Cf. apply continuity_2d_pt_filterlim. apply filterlim_comp with (1 := Cf). apply (filterlim_Rbar_inv (f x y)). contradict Df. now injection Df. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq