proposition: Lemma even_halfB 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 -doubleB doubleK. Qed.
imports: mathcomp(all_ssreflect finmap)