fact: Definition prec : relation A := fun f g => match f, g with | nat_0, nat_S => True | nat_0, ord_zero => True | nat_0, ord_cons => True | nat_0, ord_psi => True | ord_zero, nat_S => True | ord_zero, ord_cons => True | ord_zero, ord_psi => True | nat_S, ord_cons => True | nat_S, ord_psi => True | ord_cons, ord_psi => True | _, _ => False end.
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