proposition: Lemma dvdn_double_leq m n : m %| n -> odd m -> ~~ odd n -> 0 < n -> m.*2 <= n.
proof: Proof. move=> m_dv_n odd_m even_n n_gt0. by rewrite -muln2 dvdn_leq // Gauss_dvd ?coprimen2 ?m_dv_n ?dvdn2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)