proposition: Lemma sternD_1n_small n (S := sternD 1 n.+2) (C := fun a b => exists i k, [/\ i < 2^k, a = nth 0 (S k) i & b = nth 0 (S k) i.+1]) a b: C a b -> C b a -> False.
proof: Proof. move => [i [k [pa pb pc]]] [j [l [qa qb qc]]]. move: pb pc; rewrite (sternD_1n_v _ (ltnW pa)) (sternD_1n_v n.+1 pa). move: qb qc; rewrite (sternD_1n_v _ (ltnW qa)) (sternD_1n_v n.+1 qa). have pd: i < 2 ^ (k + n.+1). by rewrite expnD; apply: (leq_trans pa) ;rewrite leq_pmulr // expn_gt0. have qd: j < 2 ^ (l + n.+1). by rewrite expnD; apply: (leq_trans qa) ;rewrite leq_pmulr // expn_gt0. move:(ltnW pd)(ltnW qd) => pd' qd'. rewrite !nth_stern11 // (addnS _ j) (addnS _ i) !sternD_fusc. set x := 2 ^ (k + n.+1) + i; set y := 2 ^ (l + n.+1) + j. move => qb qc pb pc. set p := 2 ^ (k + n.+1). have la : p <= x by rewrite /p/x leq_addr /=. have lb : x < p.*2 by rewrite /p/x - addnn ltn_add2l. have lc: p <= x <= p.*2 by rewrite la (ltnW lb). have ld: p <= x.+1 <= p.*2 by rewrite lb andbT ltnW. pose x' := 3 * p - x.+1. have ea: x.+1 + x' = 3 * p. apply: subnKC. apply: (leq_trans lb); rewrite -mul2n. by apply: leq_pmul2r; rewrite expn_gt0. have eb: x + x'.+1 = 3 * p by rewrite - addSnnS ea. have ly:log2 y = (l + n.+1).+1. by apply: log2_pr; rewrite expn2S - addnn ltn_add2l leq_addr qd. have lx:log2 x' = (k + n.+1).+1. apply: log2_pr; rewrite expn2S -/p - (leq_add2l p.*2) -(ltn_add2l p) addnC. by rewrite -mul2n -mulSn - ea leq_add2r ltn_add2r mul2n lb ltnS la. move:(fusc_palindrome lc eb) (fusc_palindrome ld ea). rewrite - pb - pc qc qb => sa sb. move: (fuscp_injective sb sa) => ec. have kl: l = k by apply/eqP; rewrite -(eqn_add2r n.+1) - eqSS -lx - ly ec. have ha: y < 2 ^ (k + n.+1) + 2 ^k by rewrite -kl /y ltn_add2l. have hb: 2 ^ k <= (2 ^ (k + n.+1)).*2. by rewrite -expn2S leq_exp2l // - addnS leq_addr. have hc:2 ^ (k + n.+1) + 2 ^ k <= (2 ^ (k + n.+1)).*2 - 2 ^ k. rewrite -(leq_add2l (2^k)) subnKC // addnCA -addnn addnn leq_add2l. by rewrite - expn2S -addSnnS leq_exp2l // leq_addr //. have hd: (2 ^ (k + n.+1)).*2 - 2 ^ k <= x'. rewrite - (leq_add2r (2^k)) (subnK hb) - (leq_add2l x.+1) addnA ea. by rewrite -/p mulSn mul2n addnAC leq_add2r /x ltn_add2l. by move: (leq_trans ha (leq_trans hc hd)); rewrite ec ltnn. 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)