proposition: Lemma T1nf_cons_cons a n a' n' b' : T1nf (cons a n (cons a' n' b')) -> a' < a.
proof: Proof. by rewrite /= T1ltn0 !if_same if_simpl => /and3P [_ _]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)