proposition: Lemma oddB m n : n <= m -> odd (m - n) = odd m (+) odd n.
proof: Proof. by move=> le_nm; apply: (@canRL bool) (addbK _) _; rewrite -oddD subnK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring