proposition: Lemma T1lt_trans b a c: a < b -> b < c -> a < c.
proof: Proof. elim: c a b => [a [] // | a'' Ha n'' c'' Hc a [] ]; rewrite ? T1ltn0 //. move => a' n' b'; case: a => // a n b /=. case: (T1ltgtP a a') => h1 //. case: (T1ltgtP a' a'') => h2 //; first by rewrite (Ha _ _ h1 h2). by rewrite - h2 h1. rewrite h1; case: (T1ltgtP a' a'') => // _; case: (ltngtP n n')%N => // h2. case: (ltngtP n' n'') => h3 //; first by rewrite (ltn_trans h2 h3). by rewrite - h3 h2. by rewrite h2; case: (ltngtP n' n'') => h3 //; apply: Hc. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)