proposition: Lemma lt_tail a b n c: T2nf (cons a b n c) -> c < cons a b n c.
proof: Proof. move /and4P => [_ _ _ h]; apply: (T2lt_le_trans h (T2le_psi1 a b n c)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)