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