Add posnum instances for ratio lemmas

[mkerjean]

https://github.com/mkerjean/analysis/blob/861206918c18ffa079680b4b7b2ad6bec3d6aada/classical/mathcomp_extra.v#L103-L114

Lemma divDl_ge0 (R : numDomainType) (s t : R) (s0 : 0 <= s) (t0 : 0 <= t) :
  0 <= s / (s + t).
Proof.
by apply: divr_ge0 => //; apply: addr_ge0.
Qed.

Lemma divDl_le1 (R : numFieldType) (s t : R) (s0 : 0 <= s) (t0 : 0 <= t) :
  s / (s + t) <= 1.
Proof.
move: s0; rewrite le0r => /predU1P [->|s0]; first by rewrite mul0r.
by rewrite ler_pdivrMr ?mul1r ?lerDl // ltr_wpDr.
Qed.

[mkerjean]

@t6s ping