proposition: Lemma onem_lt r s : (r < s) = (`1-s < `1-r).
proof: Proof. apply/idP/idP => [rs|]; first by rewrite ler_ltB. by rewrite ltrBrDl addrCA -ltrBrDl subrr subr_lt0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)