proposition: Lemma pair_le_lt_trans n m p: m != NaN -> m <= n -> n < p -> m < p.
proof: Proof. rewrite /pair_le /pair_lt => mz sa sb. case: (posnP n.2) => n2z; first by move: sb; rewrite n2z ltn0. case (posnP m.2) => m2z. move: sa; rewrite m2z leqn0 muln_eq0 (gtn_eqF n2z) orbF => m1z. by move: mz; rewrite (surjective_pairing m) m2z (eqP m1z). move:(leq_mul2r p.2 (m.1 * n.2) (m.2 * n.1)); rewrite sa orbT => sa'. move: sb; rewrite - (ltn_pmul2l m2z) mulnA => sb'. by move: (leq_ltn_trans sa' sb'); rewrite mulnAC (mulnC n.2) mulnA ltn_pmul2r. 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)