proposition: Lemma pair_near_good a b: pair_near a b -> good_pair a && good_pair b.
proof: Proof. rewrite pair_nearE => /eqP H. apply/andP; split; last exact:(coprime_if_bezout H). by move:H; rewrite mulnC (mulnC a.1) => /coprime_if_bezout; rewrite coprime_sym. 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)