proposition: Lemma leq_half_double m n : (m./2 <= n) = (m <= n.*2.+1).
proof: Proof. apply/idP/idP => [m2Ln|mLnn]; last first. by rewrite -[n](half_bit_double _ true) half_leq. rewrite -[m](odd_double_half) -add1n. by apply: leq_add; [case: odd|rewrite leq_double]. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)