proposition: Lemma trunc_log2S n : 1 < n -> trunc_log 2 n = (trunc_log 2 n./2).+1.
proof: Proof. move=> n_gt1. rewrite -trunc_log2_double ?half_gt0//. rewrite -[n in LHS]odd_double_half. case: odd => //; rewrite add1n. apply: trunc_log_eq => //. rewrite leqW ?trunc_logP //= ?double_gt0 ?half_gt0//. rewrite trunc_log2_double ?half_gt0// expnS. by rewrite -doubleS mul2n leq_double trunc_log_ltn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)