fact: Definition sup_of (f: T3-> T3) x z := [/\ T3nf z, (forall y, T3nf y -> y < x -> f y <= z) & (forall z', T3nf z' -> z' < z -> exists y, [&& T3nf y, y < x & z' < f y])].
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)