proposition: Theorem rZltDef2 : forall a b : rZ, rZlt a b -> ~ eqRz a b.
proof: Proof. intros a b H; unfold eqRz in |- *; apply rltDef2; auto with stalmarck. Qed.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)