proposition: Lemma onem_div r s : s != 0 -> `1-(r / s) = (s - r) / s.
proof: Proof. by rewrite !onemE => q0; rewrite mulrDl mulNr divff. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)