Proof of "less than or equal" transitive law in Coq

I recently started learning Coq at a university course. I have an assignment with a problem, and I got stuck. I need to demonstrate the transitivity of the <= law, which states that for all m, n and p, if m <= n and n <= p, then m <= p. I tried every basic tactic possible, and I didn't figure it out. I want to mention that I'm a beginner and any basic solution without complicated tactics would be appreciated. It should be done with induction as well. Thanks!

Inductive Nat := O : Nat | S : Nat -> Nat.

Fixpoint le_Nat (m n : Nat) : bool :=
  match m with 
  | O => true
  | S m' => match n with 
            | O => false
            | S n' => (le_Nat m' n')
            end
  end.

Lemma le_Trans :
  forall m n p,
    le_Nat m n = true -> le_Nat n p = true -> le_Nat m p = true.
Proof.
    ...
Qed.

Solution

Here is a long, detailled version:

Proof.
  induction m as [| m IHm]; simpl.     
  - reflexivity.
  - destruct n; simpl. 
   + intros; discriminate.
   + destruct p; simpl. 
    * intros; assumption. 
    * apply IHm. 
Qed.

and a shorter one:

induction m;destruct n; destruct p; simpl; try (reflexivity || discriminate).
apply IHm. 
Qed.