proposition: Lemma eqA_equivalence : equivalence A eqA.
proof: Proof. inversion leA_preorder. split. intro a; split; apply preord_refl. intros a b c H1 H2. elim H1; clear H1; intros a_le_g b_le_a. elim H2; clear H2; intros b_le_c c_le_b. split. apply preord_trans with b; hyp. apply preord_trans with b; hyp. intros a b H. elim H; split; hyp. Qed.
imports: CoLoR(LogicUtil) Coq(Relations)