proposition: Lemma T2gt1 x: (one < x) = ((x != zero) && (x != one)).
proof: Proof. case: (T2ltgtP x one); rewrite ? andbT ? andbF //; last by case: x. by rewrite T2lt1 => ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)