proposition: Lemma le_contract : {mono contract : x y / (x <= y)%O}.
proof: Proof. apply: le_mono; move=> -[r0 | | ] [r1 | _ | _] //=. - rewrite lte_fin => r0r1; rewrite ltr_pdivrMr ?ltr_wpDr//. rewrite mulrAC ltr_pdivlMr ?ltr_wpDr// 2?mulrDr 2?mulr1. have [r10|?] := ler0P r1; last first. rewrite ltr_leD // mulrC; have [r00|//] := ler0P r0. by rewrite (@le_trans _ _ 0%R) // ?pmulr_rle0// mulr_ge0// ?oppr_ge0// ltW. have [?|r00] := ler0P r0; first by rewrite ltr_leD // 2!mulrN mulrC. by move: (le_lt_trans r10 (lt_trans r00 r0r1)); rewrite ltxx. - by rewrite ltr_pdivrMr ?ltr_wpDr// mul1r ltr_pwDl // ler_norm. - rewrite ltr_pdivlMr ?mulN1r ?ltr_wpDr// => _. by rewrite ltrNl ltr_pwDl // ler_normr lexx orbT. - by rewrite -subr_gt0 opprK. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed