Fix implicit arguments for sign predicates in `Data.Rational(.Unnormalised).Properties`

Unlike in `Data.Nat` or `Data.Integer`, it is not possible to infer for Agda to infer `p` from e.g. `Positive p`. We should go through and check that all proofs that use the sign predicates have such `p`'s as explicit rather than implicit arguments. Might be good to add a comment to this effect by the definition of the predicates as well.