proposition: Lemma DH_power_two k n: s (2 ^ n * k) = s k.
proof: Proof. rewrite - DH_FR - (DH_FR k); congr s; elim:n => //. by rewrite mul1n. by move => n <-; rewrite expnS - mulnA mul2n base2rev_even. 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)