proposition: Lemma even_halfMr k m : ~~ odd m -> (m * k)./2 = m./2 * k.
proof: Proof. move=> mE. have := odd_double_half m; rewrite (negPf mE) add0n => {1}<-. by rewrite -doubleMl doubleK. Qed.
imports: mathcomp(all_ssreflect finmap)