`conv_gt0` as an instance of `PosNum`

[affeldt-aist]

analysis/theories/convex.v

Line 138 in 7880978

Lemma conv_gt0 (a b : R^o) (t : {i01 R}) : 0 < a -> 0 < b -> 0 < a <| t |> b.

"make this an instance of PosNum"

[affeldt-aist]

"I guess you should take inspiration from min and max in signed.v" (@proux01 )