proposition: Lemma DH_palindrome i a b: let p := 2 ^ i in p <= a <= p.*2 -> a + b = 3 * p -> s a = s b.
proof: Proof. move => /= /andP [le1 le2] eq1. have H k: s k.*2 = s k by rewrite - DH_FR base2rev_even DH_FR. move: le2; rewrite leq_eqVlt; case/orP => le2. move /eqP:eq1; rewrite (eqP le2) (mulnDl 2 1) mul1n mul2n eqn_add2l. by move/eqP ->. have /log2_pr loga: 2 ^ i <= a < 2 ^ i.+1 by rewrite expnS mul2n le1 le2. move: le1; rewrite leq_eqVlt; case/orP => le1. move /eqP:eq1; rewrite (eqP le1) (mulnDl 1 2) mul1n mul2n eqn_add2l. by move/eqP ->. have /bin_invert_p1: 2 ^ (log2 a).-1 < a by rewrite loga. by move/eqP; rewrite loga - eq1 eqn_add2l => /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)