proposition: Lemma areaN_lt a b: a < b -> (areaN a b)%:Z = area a b.
proof: Proof. rewrite /areaN /area => /ltnW h; apply: (addrI (a.1 * b.2)%:Z). by rewrite - PoszD subnKC // -!PoszM addrA addrC addKr. 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)