proposition: Lemma T2le_psi1 a b n c: [a, b] <= cons a b n c.
proof: Proof. by rewrite T2le_consE /lt_psi ! T2ltnn !eqxx // T2le0n /=; case: n. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)