fact: Definition trichotomy_inf : forall t t', {t < t'}+{t=t'}+{t'< t}.
imports: EPSILON0 Arith List Omega Compare_dec Relations Wellfounded Max Tools More_nat AccP not_decreasing EPSILON0 More_nat Gamma0_prelude Gamma0_length term rpo