proposition: Lemma maxeMr z x y : z \is a fin_num -> 0 < z -> z * maxe x y = maxe (z * x) (z * y).
proof: Proof. move=> + r0; have [xy|yx|->] := ltgtP x y; last by rewrite maxxx. - by move=> zfin; rewrite /maxe lte_pmul2l // xy. - by move=> zfin; rewrite maxC /maxe lte_pmul2l// yx. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed