proposition: Lemma lt_succ_succ x y: T1succ x < T1succ y -> x < y.
proof: Proof. elim: x y; first by case; [ rewrite T1ltnn | move => a n b _ ]. move => a _ n b Hb; case; [ by case a | move => a' n' b']. case a;case a' => //; first by rewrite /= ltnS if_same; case: (n < n')%N. move => a'' n'' b'' a''' n''' b'''; rewrite /= T1eqE. case (T1ltgtP a''' a'') => //;case (ltngtP n''' n'') => //. case (T1ltgtP b''' b'') => //;case (ltngtP n n') => //= _ _ _ _; apply: Hb. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)