proposition: Lemma leq_uphalf_e2n n m : n <= `2^ m.+1 -> uphalf n <= `2^ m.
proof: Proof. rewrite -{1}(odd_double_half n) uphalf_half e2Sn addnn. by case: odd; rewrite //= ?add1n ?ltn_double // leq_double. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)