Theorem nle_refl

Proof
nle_refl. ⊢ a ∈ ℕ → a ≤ a,
  pred_restr nat_incl_in_real rle_refl.

Dependencies
The given proof depends on five axioms:
comp, eq_subst, radd_closed, real_is_set, rle_refl.