proposition: Lemma T3ge1 x: (one <= x) = (x != zero).
proof: Proof. by case: x => //; case => //; case => //; case => //; case => //; case. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)