proposition: Lemma compare_reflect : forall c c', match compare c c' with | Lt => c < c' | Eq => c = c' | Gt => c' < c end.
proof: Proof. unfold compare. intros; case (trichotomy_inf c c');auto. destruct s;auto with T2. Qed.
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