proposition: Lemma half_ltn_double m n : m < n.*2 -> m./2 < n.
proof: Proof. move => H. rewrite -ltn_double. rewrite -(odd_double_half m) in H. rewrite -(ltn_add2l (odd m)). by apply ltn_addl. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div)