proposition: Theorem lt_trans : transitive A lt.
proof: Proof. 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; now apply D.lt_le_weak. Qed.
imports: Relations List ZArith