proposition: Theorem compare_reflectR : forall a b : T1, (match trichotomy_inf a b with inleft (left _) => Datatypes.Lt | inleft (right _) => Datatypes.Eq | inright _ => Gt end) = compare a b.
proof: Proof. intros c1 c2;case (trichotomy_inf c1 c2). destruct s; auto; try discriminate. rewrite compare_rw1;auto. subst c1;rewrite compare_rw2;auto. intro; rewrite compare_rw3;auto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List