proposition: Lemma sup_unique f x z z': sup_of f x z -> sup_of f x z' -> z = z'.
proof: Proof. move => [pa pb pc] [pa' pb' pc']; case (T3ltgtP z z') => // sa. move: (pc' z pa sa) => [y /and3P [ya yb yc]]. by move: (pb _ ya yb); rewrite (T3leNgt) yc. move: (pc _ pa' sa) => [y /and3P [ya yb yc]]. by move: (pb' _ ya yb); rewrite (T3leNgt) yc. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)