proposition: Lemma onem_le r s : (r <= s) = (`1-s <= `1-r).
proof: Proof. apply/idP/idP => [|?]; first exact: lerB. by rewrite -(opprK r) lerNl -(lerD2l 1). Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)