Two trivial facts on natural numbers in Coq.

nat-examples.v

Goal 1 > 0.
  apply le_n.
Qed.

Goal forall n, S n > 0.
  (* What is gt? *)
  Print gt.
  (*
    gt = fun n m : nat => m < n
     : nat -> nat -> Prop
  *)
  (* It is just less-than. Let us open the definition of gt. *)
  unfold gt.
  (* What is lt? *)
  Print lt.
  (*
  lt = fun n m : nat => S n <= m
     : nat -> nat -> Prop
  *)
  (* Fun, it's just defined in terms of less-than-equal, open it. *)
  unfold lt.
  (* Then, what is le? *)
  Print le.
  (*
    Inductive le (n : nat) : nat -> Prop :=
    | le_n : n <= n
    | le_S : forall m : nat, n <= m -> n <= S m
  *)
  (* Less-than-equal is defined inductively, exactly like a `nat`. *)
  (* There are two constructors/axioms that build le,
     le_n and le_S. If we want to build an le, we must do a
     proof by induction, because to use le_S we need an assumption
     with le, which we currently do not have. *)
  induction n.
  - (* Base case: 1 <= 1 *)
    apply le_n.
  - (* Inductive step: 1 <= S (S n) *)
    (* IH: 1 <= S n *)
    apply le_S.
    (* We are ready to use the IH. *)
    assumption.
Qed.