proposition: Lemma lt_intro : forall a b, compare a b = Datatypes.Lt -> a < b.
proof: Proof. intros a b; rewrite <- compare_reflectR. case (trichotomy_inf a b);auto with T1. destruct s; auto. discriminate 1. discriminate 2. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List