proposition: Lemma pair_distl x a b: a < b -> a < x -> x < a + b -> (pair_dist x a (a+b)%nat_pair < pair_dist x a b) %N.
proof: Proof. move => lab sa sb. move:(pair_add_smonotone lab) => /andP [_ sc]; move:(pair_lt_trans sb sc) => sd. have: pair_dist x a (a + b) = areaN x b :> int. by rewrite /pair_dist areaN_lt // PoszD !areaN_lt // area_Dr area_sym addKr. by case => ->; apply: ltn_paddl; rewrite/areaN subn_gt0. 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)