proposition: Lemma prec_transitive : transitive A prec.
proof: Proof. intros s1 s2 s3; destruct s1; destruct s2; destruct s3; simpl; intros; trivial; contradiction. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List