proposition: Lemma area_eq0 a b: good_pair a -> good_pair b -> (area a b) == 0 -> a = b.
proof: Proof. move => sa sb; rewrite Order.POrderTheory.eq_le {1} area_sym oppr_le0 - !area_ge0 => h. by move:(esym(pair_le_anti sb sa)); rewrite h => /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)