proposition: Lemma natnat_to_nat3K: cancel natnat_to_nat3_inv natnat_to_nat3.
proof: Proof. have Hb l: (l== nil) || ends_with_a l true -> (list_of_num (bin_of_nat (nat_of_list l))) = l. case /orP; first by move/eqP ->. by move => H; rewrite (nat_of_list_rT' H) nat_of_binK num_of_listK'. case => // n. rewrite /natnat_to_nat3 /natnat_to_nat3_inv. move:(nat_list_succ' n); set l := list_of_num _ => /= lp. have ->: n.+1 = nat_of_bin (num_of_list l). by rewrite /l list_of_numK /= pos_of_natK. move: (nn_to_n_check_end (nn_to_n_split l).1) => [w1 [k1 [eql1 prop1]]]. move: (nn_to_n_check_end (nn_to_n_split l).2) => [w2 [k2 [eql2 prop2]]]. rewrite eql1 eql2 !nat_of_list_ext (Hb _ prop1) (Hb _ prop2). move: (nn_to_n_merge_ext w1 w2 k1 k2); rewrite -eql1 -eql2 => eql3. move:(f_equal nat_of_list (nn_to_n_splitK l)); rewrite /= eql3 !nat_of_list_ext. by move => ->; rewrite -(nat_of_list_rT' lp). 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)