proposition: Lemma so_not_symmetric : forall a b, R a b -> R b a -> False.
proof: Proof. unfold not; intros a b Rab Rba. exact (sord_irrefl so (sord_trans so Rab Rba)). Qed.
imports: Coq(Arith Setoid Morphisms Basics ZArith) CoLoR(LogicUtil RelUtil)