proposition: Lemma realMr x y : x != 0 -> x \is real -> (x * y \is real) = (y \is real).
proof: Proof. move=> x_neq0 xR; case: real_ltgtP x_neq0 => // hx _; rewrite !realE. by rewrite nmulr_rge0 // nmulr_rle0 // orbC. by rewrite pmulr_rge0 // pmulr_rle0 // orbC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)