proposition: Lemma compare_reflect : forall a a', match compare a a' with | Datatypes.Lt => a < a' | Datatypes.Eq => a = a' | Datatypes.Gt => a' < a end.
proof: Proof. intros c c'; case (compare_ok_1 c c');intros H0 H1; case H0; case H1; intros; caseEq (compare c c'); auto. intro comp; case (trichotomy_inf c c'). intro x; case x; intro H'. rewrite (H4 H') in comp;discriminate comp. rewrite (H2 H') in comp;discriminate comp. trivial. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List