proposition: Lemma lee_ndivl_mulr r x y : (r < 0)%R -> (x <= y * r^-1%:E) = (y <= x * r%:E).
proof: Proof. rewrite -oppr0 ltrNr => r0; rewrite -{1}(opprK r) invrN. by rewrite EFinN muleN leeNr lee_pdivr_mulr// EFinN muleNN. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed