proposition: Lemma psi_lt1 a b c d n a' b' c': cons a b c n d < [a', b', c'] = ([a, b,c] < [a', b', c']).
proof: Proof. by rewrite T3lt_consE T3lt_psi T3ltn0 ! if_same if_simpl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)