proposition: Lemma trichotomy : forall a b, a < b \/ a = b \/ b < a.
proof: Proof. intros a b; case (trichotomy_inf a b); auto. destruct 1;auto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List