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 | ord_zero, nat_S => True | ord_zero, ord_cons => True | nat_S, ord_cons => True | _, _ => False end.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List