proposition: Lemma geq_half_double m n : (m <= n./2) = (m.*2 <= n).
proof: Proof. rewrite -[X in _.*2 <= X]odd_double_half. case: odd; last by rewrite leq_double. by case: m => // m; rewrite doubleS ltnS ltn_double. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring