proposition: Lemma compare_rw1 : forall a b, a < b -> compare a b = Datatypes.Lt.
proof: Proof. intros c1 c2; generalize (compare_reflect c1 c2). case (compare c1 c2);auto. intros e H;subst c2;case (lt_irr H). intros H1 H2;case (lt_not_gt H2);auto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List