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