proposition: Lemma pair_le_trans n m p: n != NaN -> m <= n -> n <= p -> m <= p.
proof: Proof. rewrite /pair_le => nz sa sb. move:(leq_mul2r p.2 (m.1 * n.2) (m.2 * n.1)); rewrite sa orbT => sa'. move:(leq_mul2l m.2 (n.1 * p.2) (n.2 * p.1)); rewrite sb orbT mulnA => sb'. move: (leq_trans sa' sb'); rewrite mulnAC (mulnC n.2) mulnA leq_mul2r. case dz: (n.2==0%N) => // _. move: sb; rewrite (eqP dz) leqn0 muln_eq0; case/orP => /eqP hb. move: sa; rewrite hb muln0 leqn0 muln_eq0 ; case/orP => /eqP hc. by rewrite hc. by move: nz; rewrite (surjective_pairing n) hb hc. by rewrite hb muln0. 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)