proposition: Theorem ZleLe : forall x y : nat, (Z_of_nat x <= Z_of_nat y)%Z -> x <= y.
proof: Proof. intros x y H'. case (Nat.le_gt_cases x y); auto with arith. intros H'0; contradict H'; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz