proposition: Lemma sup_unique f x z z': sup f x z -> sup f x z' -> z = z'.
proof: Proof. move => [pa pb pc] [pa' pb' pc']; case (T1ltgtP z z') => //. move/(pc' _ pa) => [y /and3P [qa qb qc]]. by move: (pb _ qa qb); rewrite T1leNgt qc. move/(pc _ pa') => [y /and3P [qa qb qc]]. by move: (pb' _ qa qb); rewrite T1leNgt qc. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)