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