docs#ennreal.coe_nonneg

Stream: general

[Yaël Dillies]

Why does docs#ennreal.coe_nonneg exist? Both sides are always true :thinking:

[Jireh Loreaux]

To remove the cast with norm_cast? :shrug:

[Yaël Dillies]

@Sebastien Gouezel, git blames you for #464.

[Sebastien Gouezel]

You have my blessing to remove it!

[Damiano Testa]

I would like to point out that both sides being always true is not necessarily a reason for a lemma being superfluous: docs#not_false_iff.

[Damiano Testa]

In this specific case, though, I agree that this lemma is probably superfluous! :smile:

[Eric Wieser]

Arguably those lemmas are superfluous anyway, as simp I think knows how to convert things to ↔ true form

[Eric Rodriguez]

(docs#iff_true + docs#true_iff)

[Eric Wieser]

(I meant in the other direction, IIRC simp can use lemma foo : P to rewrite f P to f true)