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