proposition: Lemma natnat_to_nat3_invK: cancel natnat_to_nat3 natnat_to_nat3_inv.
proof: Proof. have Hc a: nat_of_list (list_of_num (bin_of_nat a)) = a. case:a => // a. by rewrite (nat_of_list_rT' (nat_list_succ' a) ) list_of_numK bin_of_natK. move => p. rewrite /natnat_to_nat3 /natnat_to_nat3_inv. rewrite [in RHS] (surjective_pairing p). move: p.1 p.2 => a b; clear p. set qa := (list_of_num (bin_of_nat a)). set qb := (list_of_num (bin_of_nat b)). set r := (nn_to_n_merge qa qb). move: (nn_to_n_check_end r) => [w [k [rv etc]]]. have ->: (list_of_num (bin_of_nat (nat_of_list r))) = w. rewrite rv nat_of_list_ext; case/orP:etc; first by move /eqP ->. move => /ends_with_aP [v vv]. by rewrite vv nat_of_list_rT nat_of_binK num_of_listK. move: (nn_to_n_split_ext w k); simpl; set k1:= if _ then _ else _. rewrite - rv (surjective_pairing (nn_to_n_split r)) => /eqP [eqa eqb]. rewrite - (nat_of_list_ext k1 (nn_to_n_split w).1) - eqa. rewrite - (nat_of_list_ext k1 (nn_to_n_split w).2) - eqb. by rewrite /r (nn_to_n_mergeK qa qb) /= ! nat_of_list_ext ! Hc. 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)