proposition: Lemma lte_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 lteNr lte_pdivr_mulr// EFinN muleNN. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed