proposition: Lemma ltA_antisym : forall (a b : A), ltA a b -> ltA b a -> False.
proof: Proof. intros a b H1 H2. elim H1; clear H1; intros a_le_b b_neq_a. elim H2; clear H2; intros b_le_a a_neq_b. apply a_neq_b; split; hyp. Qed.
imports: CoLoR(LogicUtil) Coq(Relations)