proposition: Lemma up_log2S n : 0 < n -> up_log 2 n.+1 = (up_log 2 (n./2.+1)).+1.
proof: Proof. case: n=> // [] [|n] // _. apply: up_log_eq => //; apply/andP; split. apply: leq_trans (_ : n./2.+1.*2 < n.+3); last first. by rewrite doubleS !ltnS -[leqRHS]odd_double_half leq_addl. have /= /andP[H1n _] := up_log_bounds (isT : 1 < 2) (isT : 1 < n./2.+2). by rewrite ltnS -leq_double -mul2n -expnS prednK ?up_log_gt0 // in H1n. rewrite -[_./2.+1]/(n./2.+2). have /= /andP[_ H2n] := up_log_bounds (isT : 1 < 2) (isT : 1 < n./2.+2). rewrite -leq_double -!mul2n -expnS in H2n. apply: leq_trans H2n. rewrite mul2n !doubleS !ltnS. by rewrite -[leqLHS]odd_double_half -add1n leq_add2r; case: odd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)