proposition: Lemma gtz0_ge1 x : (0 < x) = (1 <= x).
proof: Proof. by case: (intP x). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)