proposition: Lemma trunc_log2_double n : 0 < n -> trunc_log 2 n.*2 = (trunc_log 2 n).+1.
proof: Proof. by move=> n_gt0; rewrite -mul2n trunc_logMp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)