Nontrivial term of nontrivial type

Stream: Is there code for X?

[Oliver Nash]

Is this really missing:

@[to_additive]
lemma exists_ne_one (G : Type _) [Group G] [Nontrivial G] : ∃ (g : G), g ≠ 1 := by
  obtain ⟨x, y, h⟩ := exists_pair_ne G
  exact ⟨x / y, Iff.mpr div_ne_one h⟩

[Johan Commelin]

I think that for every x, you should be able to get a y that is unequal to it.

[Johan Commelin]

That lemma should exist, and it doesn't need algebraic structure.

[Sebastien Gouezel]

docs#exists_ne

[Oliver Nash]

Right, thanks!