proposition: Lemma mulRnng_ge0 (x y : Rnng) : (0 <= (x : R) * y)%mcR.
proof: Proof. exact/RleP/mulR_ge0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR realType_ext Reals Lra mathcomp(lra)