proposition: Lemma DH_palindrome_res k: 0 < k -> exists m, [/\ (k == 1) || odd (m+k), s k = s m.+1 & s k.+1 = s m].
proof: Proof. move => knz. move: (prednK knz) => kv. move: (log2_bnd k.-1); rewrite /= {2} log2S_k kv; set i := (log2 _).-1. rewrite expnS mul2n;set p := 2 ^i; set m := 3 * p - k.+1. move => /andP[le1 le2]. have ra: k.+1 + m = 3 * p. rewrite /m addnC subnK // (mulnDl 1 2 p) mul1n mul2n. by apply:(leq_trans le2); apply: leq_addl. have rb: m.+1 +k = 3 * p by rewrite addnC - addSnnS. have le3 : p <= k.+1 <= p.*2 by rewrite le2 andbT ltnW. have rc: p <= m.+1. by rewrite -(leq_add2r k) rb (mulnDl 1 2 p) mul1n mul2n leq_add2l ltnW. have rd: m.+1 <= p.*2. by rewrite -(leq_add2r k) rb (mulnDl 2 1 p) mul1n mul2n leq_add2l. have le4: p <= m.+1 <= p.*2 by rewrite rc rd. have okm: (k == 1) || odd (m+k). move:(f_equal odd ra); rewrite addSn oddM /p oddX /= orbF. move:le2; rewrite addnC /p; case: (odd (m+k)); first by rewrite orbT. case iz: (i==0) => //. rewrite (eqP iz) /=. move: knz. clear. by case: k => //;case. exists m; split => //. by rewrite(DH_palindrome le4 rb). exact:(DH_palindrome le3 ra). 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)