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