proposition: Theorem evalZMin : forall (a : rNat) (b c : rZ), evalN a = b -> rZlt c b -> evalN a <> evalZ c.
proof: Proof. intros a b c H' H'0; Contradict H'0. rewrite <- H'; rewrite H'0. case (evalZltOr c); auto with stalmarck. intros H'1; rewrite H'1; auto with stalmarck. Qed.