Cody's answer is excellent, and fulfils your question about translating your proof to Coq. As a complement to that, I wanted to add the same results, but proven using a different route, mainly as an illustration of some bits of Coq and to demonstrate what you can prove syntactically with very little additional work. This is not a claim however that this is the shortest route - just a different one. The proofs only include one additional helper lemma, and rely only on basic definitions, I don't introduce addition, multiplication or any of their properties, or functional extensionality, and the only Peano axioms are a simple form of a <= b -> a+c <= b+c in the helper lemma (just for c=1) and structural induction, which comes with inductive types for free anyway.

Like Cody, where I thought it made no difference, I used predefined types etc., so before the proof, I'll describe those:

• I used the built in nat type for natural numbers, which has (up to precise naming) the same definition as yours:

Inductive nat : Set := O : nat | S : nat -> nat

• I used the built in le and lt for less than or equal and less than respectively, which have notational shorthands "<=" and "<" for readability. They are defined:

Inductive le : nat -> nat -> Prop :=
| le_n : forall n, le n n
| le_S : forall n m, (le n m) -> (le n (S m)).

and

Definition lt (n m:nat) := le (S n) m.

• The built in eq (shorthand "=") is syntactic equality and works the same as your "I", with one constructor that just says anything is equal to itself. The symmetric and transitive properties are easy proofs from there, but we won't need them in this case. The definition for eq below has the notation built into it.

Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x

• Lastly, I've used the propositional or (shorthand "/" - which is backslash forwardslash, it doesn't render quite clearly here, if you cut and paste into a text editor, it should be obvious), which has two constructors, basically that either you have evidence for the left argument, or the right argument. Coq also has some shorthand tactics, left and right, which just mean "apply or_introl" and "apply or_intror" respectively.

Inductive or (A B : Prop) : Prop :=
or_introl : A -> A / B | or_intror : B -> A / B

What now follows are my proofs, in principle, if markup doesn't get in the way, you should be able to just cut and past this into a Coq .v file and it will work. I've included comments to note interesting bits, but they are in (* *) delimiters, so you shouldn't have to remove them.

Theorem lt_or_eq: forall (n m : nat),
  n < S m -> n < m \/ n = m.
Proof.
(*
  This proof is just a case analysis on n and m, whether they're zero or
  a successor of something.
*)
destruct n as [|n']; destruct m as [|m']. 

(*n = 0, m = 0*)
intros.
  right. reflexivity.

(*n = 0, m = S m'*)
intros H.
  inversion H.
  inversion H1.
  left. unfold lt. constructor.
  (*The constructor tactic tries to match the goal to a constructor
    that's in the environment.*) 
  left. unfold lt. constructor. assumption.
  (*Assumption tries to match the goal to something that's in the
    current context*)

(*n = S n', m = 0
  This case is false, so we can invert our way out of it.*)
intros.
  inversion H. inversion H1.

(*n = S n', m = S m'*)
intros.
  inversion H.
    right. reflexivity.
    left. unfold lt. assumption.
Qed.


(*
  The following lemma with be useful in the proof of the trichotomy theorem,
  it's pretty obviously true, and easy to prove. The interesting part for
  anyone relatively new to Coq is that the induction is done on the
  hypothesis "a <= b", rather than on either a or b.
*)
Lemma a_le_b_implies_Sa_le_Sb: forall a b, a <= b -> S a <= S b.
Proof.
  intros a b Hyp.
  induction Hyp.
  constructor.
  constructor.
  apply IHHyp.
Qed.

(*
  The proof of the trichotomy theorem is a little more involved than the
  last one but again we don't use anything particularly tricky. 
  Other than the helper lemma above, we don't use anything other than the
  definitions.

  The proof proceeds by induction on n, then induction on m.  My personal
  feeling is that this can probably be shortened.  
*)
Theorem trich: forall (n m : nat),
  n < m \/ n = m \/ m < n.
Proof.
  induction n.
    induction m.
      right. left. reflexivity.
        inversion IHm.
          left. unfold lt. constructor. unfold lt in H. assumption.
          inversion H.
          left. unfold lt. subst. constructor.
          inversion H0.     
    induction m.
      assert (n < 0 \/ n = 0 \/ 0 < n).
      apply IHn.
      inversion H.
      inversion H0.
      inversion H0.
      right. right. subst. unfold lt. constructor.
      right. right. unfold lt. constructor. assumption.
      inversion IHm. unfold lt in H.
      left. unfold lt. constructor. assumption.
      inversion H; subst.
      left. unfold lt. constructor.
      inversion H0.
      right. left. reflexivity.
      right. right. apply lt_or_eq in H0.
    
      inversion H0.
      apply a_le_b_implies_Sa_le_Sb. assumption.
      subst. unfold lt. apply a_le_b_implies_Sa_le_Sb. assumption.
Qed.

(*
  The following is just to show what can be done with some of the tactics
  The omega tactic implements a Pressburger arithmetic solver, so anything
  with natural numbers, plus, multiplication by constants, and basic logic
  can just be solved. Not very interesting for practicing Coq, but cool to
  know.
*)

Require Import Omega.

Example trich' : forall (n m : nat),
  n < m \/ n = m \/ m < n.
Proof.
  intros.
  omega.
Qed.