proposition: Lemma realMe x y : (0%E >=< x)%O -> (0%E >=< y)%O -> (0%E >=< x * y)%O.
proof: Proof. case: x y => [x||] [y||]// rx ry; do ?[exact: realM |by rewrite /mule/= lt0y |by rewrite real_mulr_infty ?realE -?lee_fin// /Num.sg; case: ifP; [|case: ifP]; rewrite ?mul0e /Order.comparable ?lexx; rewrite ?mulN1e ?leNy0 ?mul1e ?le0y |by rewrite mulNyNy /Order.comparable le0y]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed