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