proposition: Lemma T1lt_cons_le a n b a' n' b': (cons a n b < cons a' n' b') -> (a <= a').
proof: Proof. by rewrite /T1le /=; case (T1ltgtP a a'). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)