proposition: Lemma fusc_bin_inverse_dijkstra n: fusc (bin_invert n.+1) = (fusc n.+1).
proof: Proof. rewrite -(fusciL_valn n.+1) -fusciL_valn bin_invert_alt_compat nat_of_binK. move: (aux_for_bin_invert n) => /=; set L := list_of_pos _; case. by move => [k ->]; rewrite bin_invert_correctB - cat_nseq cats1 num_of_listK. move => [k [l ->]]. rewrite bin_invert_correctA -cat_nseq -rcons_cons -rcons_cat num_of_listK. elim:k; last by move => k H; rewrite /= !fusciL_even H. rewrite /=!fusciL_odd! addn0; elim: l (1){1 4}(1). by move => a b; rewrite !fusciL_odd !fusciL_0 addnC. by move => x l H a b; case x; rewrite /= fusciL_even fusciL_odd H // addnC. 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)