proposition: Lemma eqe_pdivr_mull r x y : (r != 0)%R -> ((r^-1)%:E * y == x) = (y == r%:E * x).
proof: Proof. rewrite neq_lt => /orP[|] r0. - by rewrite eq_le lee_ndivr_mull// lee_ndivl_mull// -eq_le. - by rewrite eq_le lee_pdivr_mull// lee_pdivl_mull// -eq_le. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed