proposition: Lemma good_pair_prop a b: good_pair a -> good_pair b -> (a.1 * b.2 = a.2 * b.1)%N -> a = b.
proof: Proof. move => ga gb ea. have : a.1 %| a.2 * b.1 by rewrite - ea /dvdn modnMr. have : b.1 %| a.1 * b.2 by rewrite ea /dvdn modnMl. rewrite Gauss_dvdl // Gauss_dvdr // => sa sb. have r1: a.1 = b.1 by apply/eqP; rewrite eqn_dvd sa sb. rewrite (surjective_pairing a) (surjective_pairing b) r1. suff: b.2 == a.2 by move/eqP => ->. move/eqP: ea; rewrite r1;case/posnP: b.1 => h; last by rewrite mulnC eqn_pmul2r. by move: ga gb; rewrite /good_pair r1 h /coprime !gcd0n => /eqP -> /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)