proposition: Lemma pair_lt_trans n m p: m < n -> n < p -> m < p.
proof: Proof. rewrite {1} /pair_lt ltn_neqAle => /andP [ha hb] hc. case hd: (m== NaN); last apply: (pair_le_lt_trans (negbT hd) hb hc). by move: ha; rewrite (eqP hd). 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)