proposition: Theorem rltAntiSym : forall a b : rNat, rlt a b -> ~ rlt b a.
proof: Proof. intros a b H'; red in |- *; intros H'0; absurd (rlt a a); auto with stalmarck. apply rltTrans with (y := b); auto with stalmarck. Qed.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)