proposition: Lemma T3le_psi a b c n d: [a,b,c] <= cons a b c n d.
proof: Proof. rewrite /T3le T3lt_consE T3ltnn T3eqE !eqxx T3lt0n (eq_sym 0) (eq_sym d) /=. by case: (ltngtP n 0) => //=; case: eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)