proposition: Lemma ltA_eqA_compat_l : forall (a b b' :A), eqA b b' -> ltA b a -> ltA b' a.
proof: Proof. inversion leA_preorder. intros a b b' b_eq b_lt_a. elim b_lt_a; clear b_lt_a; intros b_le_a b_neq_a. split. elim b_eq; clear b_eq; intros b_le_b' b'_le_b. apply preord_trans with b; hyp. elim (eqA_equivalence); intros eqA_refl eqA_trans eqA_sym. intro; apply b_neq_a; apply eqA_trans with b'; trivial. Qed.
imports: CoLoR(LogicUtil) Coq(Relations)