proposition: Lemma ltA_eqA_compat_r : forall (a b b' :A), eqA b b' -> ltA a b -> ltA a b'.
proof: Proof. inversion leA_preorder. intros a b b' b_eq a_lt_b. elim a_lt_b; clear a_lt_b; intros a_le_b a_neq_b. 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 a_neq_b; apply eqA_trans with b'; trivial. elim b_eq; split; trivial. Qed.
imports: CoLoR(LogicUtil) Coq(Relations)