proposition: Lemma even_halfD m n : ~~ odd m -> ~~ odd n -> (m + n)./2 = (m./2 + n./2).
proof: Proof. move=> mE nE. have := odd_double_half m; rewrite (negPf mE) add0n => {1}<-. have := odd_double_half n; rewrite (negPf nE) add0n => {1}<-. by rewrite -doubleD doubleK. Qed.
imports: mathcomp(all_ssreflect finmap)