proposition: Lemma halfD m n : (m + n)./2 = (odd m && odd n) + (m./2 + n./2).
proof: Proof. rewrite -[n in LHS]odd_double_half addnCA. rewrite -[m in LHS]odd_double_half -addnA -doubleD. by do 2!case: odd; rewrite /= ?add0n ?half_double ?uphalf_double. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring