proposition: Lemma elogn2_unique a b a' b': (a.*2.+1) * 2 ^ b = (a'.*2.+1) * 2 ^ b' -> a = a'.
proof: Proof. move/eqP; wlog: a b a' b' / b <= b'. move =>h; case/orP: (leq_total b b') => h'; first by apply: h. by rewrite eq_sym; move /(h _ _ _ _ h'). move => la; rewrite - (subnK la) expnD mulnA eqn_pmul2r ?expn_gt0 // => /eqP h. move:(congr1 odd h); rewrite oddM /= !odd_double /= oddX orbF => ha. by move /eqP: h; rewrite (eqP (esym ha)) muln1 eqSS eqn_double => /eqP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)