proposition: Lemma natnat_to_nat2_inj: injective natnat_to_nat2.
proof: Proof. pose g a := binomial a.+1 2. pose f a b := a + g (a+b). move => p1 p2. rewrite {2} (surjective_pairing p1) {2} (surjective_pairing p2). set a1 := p1.1; set a2 := p2.1; set b1 := p1.2; set b2 := p2.2. rewrite /natnat_to_nat2 -/(f a1 b1) -/(f a2 b2) => eqa. have Ha a: g a.+1 = g a + a.+1 by rewrite /g binS bin1. have Hb a b: g (a+b) <= f a b < g((a+b).+1). by rewrite /f leq_addl /= Ha addnS ltnS addnC addnA leq_addr. have Hc a b: g a < g (b.+1) -> a <= b. case: (leqP a b) => //; rewrite -ltnS (ltnNge (g a))/g. by move/(leq_bin2l 2) ->. move: (Hb a1 b1) (Hb a2 b2); rewrite eqa => /andP[la lb] /andP[lc ld]. move: (leq_ltn_trans la ld) (leq_ltn_trans lc lb). move => /Hc l1 /Hc l2. have eqb: a1 + b1 == a2 + b2 by rewrite eqn_leq l1 l2. move /eqP: eqa; rewrite /f (eqP eqb) eqn_add2r => /eqP eqc. by move: eqb; rewrite eqc eqn_add2l => /eqP ->. 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)