proposition: Lemma maxeMl z x y : z \is a fin_num -> 0 < z -> maxe x y * z = maxe (x * z) (y * z).
proof: Proof. by move=> zfin z0; rewrite muleC maxeMr// !(muleC z). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed