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