proposition: Lemma natnat_to_nat1_bij: bijective natnat_to_nat1.
proof: Proof. have C1: cancel natnat_to_nat1_inv natnat_to_nat1. move => n. rewrite /natnat_to_nat1_inv /natnat_to_nat1. by case (elogn2P n) => e m /= <-. exists natnat_to_nat1_inv => //. apply: (inj_can_sym C1) => p q. rewrite /natnat_to_nat1. set c := _*_; set c' := _ * _. have /prednK cp: 0 < c by rewrite /c muln_gt0 expn_gt0. have /prednK cp': 0 < c' by rewrite /c muln_gt0 expn_gt0. move/(f_equal (fun t => t.+1)); rewrite cp cp' => /eqP eq_cc. rewrite (surjective_pairing p) (surjective_pairing q). move: eq_cc; rewrite /c/c'. move: p.1 p.2 q.1 q.2 => a b a' b'. wlog: a b a' b' / a <= a'. move =>h; case/orP: (leq_total a a') => h'; first by apply: h. by rewrite eq_sym; move /(h _ _ _ _ h'). move => la;rewrite - (subnKC la) expnD -mulnA eqn_pmul2l ?expn_gt0 // => /eqP h. move:(congr1 odd h); rewrite oddM /= !odd_double /= andbT oddX orbF => ha. move /eqP: h; rewrite (eqP (esym ha)) mul1n /= eqSS eqn_double addn0 => /eqP. by move => ->. 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)