import analysis.topology.topological_groups

universes u v
variables {α : Type u} {β : Type v}
variables [group α] [group β]
variables [topological_space α] [topological_space β]
variables [topological_group α] [topological_group β]
variables (f : α → β) [is_group_hom f]
variables (hf : filter.tendsto f (nhds 1) (nhds 1))
theorem cts_of_cts_at_1 : continuous f :=
continuous_iff_tendsto.2 $ λ x,
have continuous (λ y : α, y * x⁻¹),
  from continuous_mul continuous_id continuous_const,
have filter.tendsto (λ y : α, y * x⁻¹) (nhds x) (nhds 1),

import analysis.real

lemma div_pos_iff_mul_pos (x y : ℝ) (Hy : y ≠ 0) : 0 < x * y ↔ 0 < x / y :=
begin
  have H : 0 < y * y,
    rcases lt_trichotomy 0 y with H | H | H,
      exact mul_pos H H,
      exact absurd H.symm Hy,
      exact mul_pos_of_neg_of_neg H H,
  split,
    intro H1,
    have H2 : (x * y) / (y * y) = x / y,
      rw div_eq_div_iff (ne_of_gt H) Hy,
      rw mul_assoc,
    rw ←H2,
    apply div_pos H1 H,
  intro H1,
  have H2 : (x / y) * (y * y) = x * y,
    rw div_mul_eq_mul_div_comm,