proposition: Lemma lt_omega2 c a' b' c' : ([zero, zero, c] < [a', b', c']) = if ((a'== zero) && (b'==zero)) then c < c' else (c < [a', b', c']).
proof: Proof. by rewrite lt_omega1 ltnn T3ltnn !andbF orbF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)