proposition: Lemma sup_Oalpha_zero: sup id zero zero.
proof: Proof. by split; [ done | by move => y _; rewrite T1ltn0 | move => z; rewrite T1ltn0]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)