proposition: Lemma fusci_palindrome_aux u u' v a b: (u + u').+1 = 2^v -> Fusci (2 ^v + u) a b = Fusci (2^v + u') b a.
proof: Proof. elim: v u u' a b. move => u u' a b /eqP; rewrite eqSS addn_eq0; case/andP => /eqP -> /eqP ->. by rewrite ! fusci_1 addnC. move => n Hrec u u' a b;rewrite expn2S => sa. wlog: a b u u' sa / ~~(odd u) && odd u'. move => H; move: (odd_double (2 ^ n)); rewrite - {1} sa /odd -/odd oddD. case od: (odd u) => /= ou. by symmetry; apply: H => //; [ by rewrite addnC | move:ou; case (odd _)]. by apply:H => //; rewrite od /=; move:ou; case (odd _). move => /andP [h1 h2]. move: (odd_double_half u) (odd_double_half u'). rewrite (negbTE h1) h2 add0n add1n => e1 e2. move /eqP: sa; rewrite -e1 -e2 -addnS -doubleS -doubleD -doubleD eqn_double. rewrite ! addnS -doubleD fusci_even fusci_odd (addnC a) => /eqP eq1. by apply: Hrec. 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)