proposition: Lemma fuscN2_prop n: fuscN2 (bin_of_nat n) = (fusc n, fusc n.+1).
proof: Proof. case: n => [// | n]; rewrite - {2 3}(bin_of_natK n.+1) - nat_of_succ_pos /=. elim: (pos_of_nat _ _). + by move => p /= ->; rewrite /= !natTrecE fusc_even fusc_odd nat_of_succ_pos. + by move => p /= ->; rewrite /= !natTrecE fusc_even fusc_odd nat_of_succ_pos. + done. 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)