mathlib

09079525 - chore(analysis/normed/group/seminorm): use coe_nonneg instead of ℝ≥0.prop (#18833)

chore(analysis/normed/group/seminorm): use coe_nonneg instead of ℝ≥0.prop (#18833) The change in `analysis.seminorm` has already been forward-ported in https://github.com/leanprover-community/mathlib4/pull/3484 to fix an error. Presumably the other changes will prevent the corresponding errors when we get to porting these files. This is needed in Lean 4 because `.prop` is about `Subtype.val` but `.coe_nonneg` is about `NNReal.toReal`. The two are defeq (and there is a simp lemma `NNReal.val_eq_coe` to convert between them), but not reducibly equal. In Lean 3 both are just about `coe`, so the change doesn't matter. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>