proposition: Lemma pair_lt_trichot a b: good_pair a -> good_pair b -> (a < b) (+) (b < a) (+) (a == b).
proof: Proof. move => pa pb. rewrite -(pair_le_anti pa pb). rewrite /pair_le/pair_lt (mulnC b.1) (mulnC b.2). set x := (a.1 * b.2)%N; set y := (a.2 * b.1)%N. by rewrite (leq_eqVlt x)(leq_eqVlt y) eq_sym; case:(ltngtP y x). 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)