proposition: Lemma fusc_symmetry1 i n: i <= 2^n -> fusc(2^n -i) + fusc i = fusc (2^n + i).
proof: Proof. case: n; first by rewrite leqn1; case/orP => /eqP -> //. move => n l1; set p := 2^n;case/orP:(leq_total i p) => l2. have ha: p <= i + p <= p.*2 by rewrite leq_addl - addnn leq_add2r. have hb: i + p + (2 ^ n.+1 - i) = 3 * p. rewrite expn2S -addnn -/p - addnBA // addnC - addnA (addnA _ i) subnK //. by rewrite addnn -mul2n -mulSn. by rewrite -(fusc_palindrome ha hb) fusc_col_progression // (addnC p). move: (subnKC l1); set j := _ - _ => l3. have l4: j <= 2^n by rewrite - (leq_add2l i) l3 expn2S - addnn leq_add2r. have ha : p <= i <= p.*2 by rewrite /p -expn2S l1 l2. have hb: i + (j +p) = 3 * p by rewrite addnA l3 mulSnr expn2S mul2n. have hc: 2 ^ (n.+1) <= 2 ^ n.+1 + i <= (2 ^ (n.+1)).*2. by rewrite leq_addr - addnn leq_add2l. rewrite (fusc_palindrome ha hb) addnC (addnC j) - fusc_col_progression //. by symmetry;apply:(fusc_palindrome hc);rewrite addnACA l3 addnn -mul2n -mulSnr. 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)