proposition: Theorem lt_trans : transitive A lt.
proof: Proof. unfold A, transitive in |- *. intros x y z H H0. apply (lt_intro x z). apply le_trans with y; apply D.lt_le_weak; assumption. intro e; rewrite e in H. absurd (y = z). intro e'; rewrite e' in H. apply (lt_irreflexive _ H). apply le_antisym; apply D.lt_le_weak; trivial. Qed.
imports: Relations List