proposition: Theorem rltNotRefl : forall a : rNat, ~ rlt a a.
proof: Proof. intros a; unfold rlt in |- *; rewrite Pcompare_refl; red in |- *; intros; discriminate. Qed.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)