proposition: Lemma fusc_palindrome_bis u u' v w w' (aux := fun u v w => (2 ^v + u).*2.+1 *(2 ^w)): (u + u').+1 = 2 ^ v -> fusc (aux u v w) = fusc (aux u' v w').
proof: Proof. suff : forall w u v, fusc (aux u v w) = Fusci (2^v + u) 1 1. by move => H; rewrite H H => /fusci_palindrome_aux. rewrite /aux;elim {u u' v w w'}; first by move => u v;rewrite muln1 fusci_vald. by move => n Hrec u v; rewrite expnSr mulnA muln2 fusc_even 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)