proposition: Lemma psi_lt2 a b n c n' c': cons a b n' c' < cons a b n c = (if (n' < n)%N then true else if n' == n then c' < c else false).
proof: Proof. by rewrite T2lt_consE -T2lt_psi T2ltnn !eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)