proposition: Lemma T1lt_anti b a: a < b -> (b < a) = false.
proof: Proof. elim: a b; first by move => b; rewrite T1ltn0. move => a Ha n b Hb [] // a' n' b' /=. case pa: (a < a'). rewrite (Ha _ pa); case aa: (a' == a) => // _. by move: pa; rewrite (eqP aa) T1ltnn. case aa: (a== a') => //. rewrite (eqP aa) eqxx T1ltnn; rewrite (eq_sym n'); case: (ltngtP n n') => //. by move => _; apply:Hb. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)