proposition: Lemma T3lt_consE a b c n d a' b' c' n' d' : cons a b c n d < cons a' b' c' n' d' = if ([a, b, c] < [a', b', c']) then true else if ([a, b, c] == [a', b', c']) then if (n < n')%N then true else if (n == n') then (d < d') else false else false.
proof: Proof. by rewrite {1} T3ltE T3lt_psi T3eqE eqxx !andbT andbA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)