Proof in Coq that natural numbers are infinity

a.v

Theorem plus_1_n : forall n : nat, n + 1 = S n /\ S n > n.
Proof.
  intros n.
  split.
  - induction n as [| n' IHn'].
    + simpl. reflexivity.
    + simpl. rewrite <- IHn'. reflexivity.
  - induction n as [| n' IHn'].
    + simpl. apply le_n.
    + simpl. apply le_n_S. apply IHn'.
Qed.
Print plus_1_n.
> plus_1_n = fun n : nat => conj (nat_ind (fun n0 : nat => n0 + 1 = S n0) (eq_refl : 0 + 1 = 1) (fun (n' : nat) (IHn' : n' + 1 = S n') => eq_ind (n' + 1) (fun n0 : nat => S (n' + 1) = S n0) eq_refl (S n') IHn' : S n' + 1 = S (S n')) n) (nat_ind (fun n0 : nat => S n0 > n0) (le_n 1 : 1 > 0) (fun (n' : nat) (IHn' : S n' > n') => le_n_S (S n') (S n') IHn' : S (S n') > S n') n)
: forall n : nat, n + 1 = S n /\ S n > n                                          

Theorem plus_1_natural : forall n : nat, 1 + n = S n /\ S n > n.
Proof.
  intros n.
  split.
  - reflexivity.
  - apply le_n_S. apply le_n.
Qed.
Print plus_1_natural.
> plus_1_natural = fun n : nat => conj eq_refl (le_n_S n n (le_n n))
: forall n : nat, 1 + n = S n /\ S n > n