proposition: Lemma prec_dec : forall a1 a2 : A, {prec a1 a2} + {~ prec a1 a2}.
proof: Proof. intros a1 a2; destruct a1; destruct a2; ((right; intro; contradiction)||(left;simpl;trivial)). Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List