proposition: Lemma T2ltnn x: (x < x) = false.
proof: Proof. elim: x => // a Ha b Hb n c Hc. by rewrite T2lt_consE /lt_psi Ha Hb Hc ltnn !if_same !andbF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)