proposition: Lemma ltA_trans : transitive A ltA.
proof: Proof. inversion leA_preorder. intros a b c H1 H2. elim H1; clear H1; intros a_le_b a_neq_b. elim H2; clear H2; intros b_le_c b_neq_c. split. apply preord_trans with b; hyp. intro H. elim H; clear H; intros a_le_c c_le_a. apply a_neq_b; split. hyp. apply preord_trans with c; hyp. Qed.
imports: CoLoR(LogicUtil) Coq(Relations)