proposition: Lemma T2lt_neAle a b : (a < b) = (a != b) && (a <= b).
proof: Proof. by rewrite T2le_eqVlt; case h: (a < b);[ rewrite (T2lt_ne h) | case(a==b) ]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)