proposition: Lemma T2lt_consE a b n c a' b' n' c' : cons a b n c < cons a' b' n' c' = if (lt_psi a b a' b') then true else if ((a== a') && (b==b')) then if (n < n')%N then true else if (n == n') then (c < c') else false else false.
proof: Proof. by rewrite {1} T2ltE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)