proposition: Lemma T1le_consE a n b a' n' b': (cons a n b <= cons a' n' b') = if a < a' then true else if a == a' then if (n < n')%N then true else if (n == n') then b <= b' else false else false.
proof: Proof. rewrite /T1le T1eqE /=. case pa: (a<a');first by rewrite orbT. case pb: (a==a') => //; case pc: (n<n')%N;first by rewrite orbT. by case pd: (n==n'). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)