proposition: Lemma mineMr z x y : z \is a fin_num -> 0 < z -> z * mine x y = mine (z * x) (z * y).
proof: Proof. move=> fz zgt0. by rewrite -eqe_oppP -muleN [in LHS]oppe_min maxeMr// !muleN -oppe_min. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed