proposition: Fact le0x (x : T * T') : (\bot, \bot) <= x :> T * T'.
proof: Proof. by case: x => // x1 x2; rewrite leEprodlexi/= !le0x implybT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)