proposition: Lemma lt_omega1 c n d a' b' c' n' d' : cons zero zero c n d < cons a' b' c' n' d' = if ((a'== zero) && (b'==zero)) then ((c < c') || ((c==c') && ((n < n')%N || ((n==n') && (d < d'))))) else (c < [a', b', c']).
proof: Proof. rewrite T3lt_consE T3lt_psi /lt_psi !T3ltn0 !T3lt0n T3eqE eqxx !andbT /=. rewrite (eq_sym zero a') (eq_sym zero b'). case pa: (a'==zero); last by rewrite orbF if_simpl. case pb: (b'==zero); [by case: (c<c') | by rewrite /= orbF if_simpl]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)