proposition: Theorem notrltzero : forall r : rZ, ~ rVlt r zero.
proof: Proof. intros r; red in |- *; intros H'; absurd (rlt (valRz r) (valRz r)); auto with stalmarck. apply rltTransRnext2 with (m := zero); auto with stalmarck. Qed.