proposition: Lemma fuscj_reverse n: Fuscj n 0 = Fuscj 0 (base2rev n).
proof: Proof. pose R a b := (b * 2^(log2 a) + (base2rev a)). suff: forall a b, Fuscj a b = Fuscj 0 (R a b) by move => H; rewrite (H n 0). have aux b: Fuscj 0 b = Fuscj 0 (R 0 b) by rewrite /R addn0 muln1. elim/fusc_ind. + by move => b; apply: aux. + by move => b; rewrite /R muln2 addn1 fuscj_1. + case => // k Ha b. by rewrite /R base2rev_even fuscj_even log2_double expnS mulnA muln2 Ha. + move => k Ha _ b. rewrite /R base2r_odd log2_Sdouble expnS mulnA muln2 addnA - mulSnr. by rewrite fuscj_odd Ha. 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)