fact: Definition natnat_to_nat3 p := nat_of_list(nn_to_n_merge (list_of_num (bin_of_nat p.1)) (list_of_num (bin_of_nat p.2))).
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)