proposition: Lemma pair_lt_le a b: good_pair a -> good_pair b -> a < b = (a <= b) && (a != b).
proof: Proof. move => sa sb. rewrite /pair_lt /pair_le ltn_neqAle andbC. case:eqP =>h; first by rewrite (good_pair_prop sa sb h) eqxx. by case:eqP => eab //; move:h; rewrite eab mulnC. 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)