proposition: Lemma lt0x x : (\bot < x) = (x != \bot).
proof: Proof. by rewrite lt_neqAle le0x andbT eq_sym. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)