proposition: Lemma compare_rw2 : forall a, compare a a = Datatypes.Eq.
proof: Proof. intro c; generalize (compare_reflect c c). case (compare c c);auto; intro H;case (lt_irr H);auto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List