proposition: Lemma natnat_to_nat2_bij: bijective natnat_to_nat2.
proof: Proof. suff C1: cancel natnat_to_nat2_inv natnat_to_nat2. exists natnat_to_nat2_inv => //. by apply: (inj_can_sym C1); apply: natnat_to_nat2_inj. move => n; rewrite /natnat_to_nat2_inv. set m := Nat.sqrt _. set s := if m * m.+1 <= n.*2 then m else m.-1. suff /andP[ha hb]: 'C(s.+1, 2) <= n < 'C(s .+2, 2). have eq1: n - 'C(s.+1, 2) <= s. rewrite - (leq_add2r 'C(s.+1, 2)) (subnK ha). by move: hb; rewrite binS bin1 addnS ltnS addnC. by rewrite /natnat_to_nat2 /= subnKC // subnK. have bind k: 'C(k.+1,2).*2 = k * k.+1. elim:k => // k hr. by rewrite binS bin1 doubleD hr - mul2n - mulnDl addn2 mulnC. have/andP[sa sb]: m^2 <= n.*2 < m.+1^2 by move: (PeanoNat.Nat.sqrt_spec' n.*2)=> [/leP -> /leP ->]. rewrite /s. case: (leqP (m * m.+1)(n.*2)) => ha. rewrite - leq_double bind ha /= -leq_double bind doubleS mulSn mulnS !addSn. move: sb; rewrite - mulnn !mulnS mulSn addSn !ltnS => h. by apply:(leq_trans h); apply: leq_addl. have mp: m = m.-1.+1 by move: ha; case:(m). rewrite - mp -leq_double - (leq_double n.+1) bind doubleS ltn_neqAle ha. have ->:n.*2.+1 != m * m.+1. by apply /negP; move /eqP /(f_equal odd); rewrite -bind /= !odd_double. move: sa; rewrite mp bind -mulnn mulSnr => sa; rewrite(leq_trans _ sa) //. apply: leq_addr. 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)