proposition: Lemma T2le_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. rewrite /T2le T2lt_consE. case pa: (lt_psi a b a' b'); first by rewrite orbT. rewrite T2eqE; case pb: (a==a') => //; case pc: (b==b') => //=. case (ltngtP n n') => //. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)