proposition: Lemma odd_geq m n : odd n -> (m <= n) = (m./2.*2 <= n).
proof: Proof. move=> odd_n; rewrite -[m in LHS]odd_double_half -[n]odd_double_half odd_n. by case: (odd m); rewrite // leq_Sdouble ltnS leq_double. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring