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