proposition: Lemma pair_nearE a b: (pair_near a b) = (a.2 * b.1 == a.1 * b.2 +1)%N.
proof: Proof. by rewrite /pair_near/area - eqz_nat subr_eq addrC PoszD !PoszM. 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)