(*#* ***Addition and multiplication
Because addition and multiplication preserve positivity, we can define
them on this subsetoid.
*)
(*#* ***Addition and multiplication
Because addition and multiplication preserve positivity, we can define
them on this subsetoid.
*)