proposition: Theorem rltDef2 : forall m n : rNat, rlt m n -> m <> n.
proof: Proof. unfold rlt in |- *; intros m n H'; red in |- *; intros H'0; rewrite <- H'0 in H'; rewrite Pcompare_refl in H'; discriminate. Qed.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)