proposition: Lemma elogn2P n : elogn2_spec n.+1 (elogn2 0 n n).
proof: Proof. rewrite -[n.+1]mul1n -[1]/(2 ^ 0) -[n in _ * n.+1](addKn n n) addnn. elim: n {1 4 6}n {2 3}0 (leqnn n) => [|q IHq] [|[|r]] e //=; last first. by move/ltnW; apply: IHq. rewrite subn1 prednK // -mul2n mulnA -expnSr. by rewrite -[q in _ * q.+1](addKn q q) addnn => _; apply: IHq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)