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