nonempty quotient

Stream: general

[Patrick Massot]

Do we already have something like:

lemma nonempty_quotient_iff {α : Type*} (s : setoid α) : nonempty (quotient s) ↔ nonempty α :=
begin
  split ; rintro ⟨c⟩,
  { cases quotient.exists_rep c with a h,
    exact ⟨a⟩ },
  { exact ⟨⟦c⟧⟩ }
end

[Simon Hudon]

That would be in data/quot and I don't see it there.