proposition: Lemma pair_lt_le_trans n m p: p != NaN -> m < n -> n <= p -> m < p.
proof: Proof. rewrite /pair_le /pair_lt => pz sa sb. move:(leq_mul2l m.2 (n.1 * p.2) (n.2 * p.1)); rewrite sb orbT mulnA => sb'. case: (posnP m.2) => m2z; first by move: sa; rewrite m2z ltn0. case: (posnP n.1) => n1z; first by move: sa; rewrite n1z muln0 ltn0. case: (posnP p.1) => p1z. move:sb; rewrite p1z muln0 leqn0 muln_eq0 (gtn_eqF n1z) /= => ww. by move: pz; rewrite (surjective_pairing p) p1z (eqP ww). case: (posnP p.2) => p2z; first by rewrite p2z muln0 muln_gt0 m2z p1z. case: (posnP n.2) => n2z. by move: sb; rewrite n2z leqn0 muln_eq0 (gtn_eqF p2z) (gtn_eqF n1z). move: sa; rewrite - (ltn_pmul2r p2z) => sa'. by move:(leq_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)