Simple example of the cut rule in Coq with and without the using the cut rule from Coq Art

ex3_5.v

(* exercise 3.5 from Coq Art *)

Section section_for_cut_example.
  Variables P Q R T : Prop.

  Hypotheses (H  : P -> Q)
             (H0 : Q -> R)
             (H1 : (P -> R) -> T -> Q)
             (H2 : (P -> R) -> T).

  Theorem cut_example : Q.
  Proof.
    cut (P -> R).
    intro H3.
    apply H1; [assumption | apply H2; assumption].
    intro H3; apply H0; apply H; assumption.
  Qed.
  
  Theorem cut_example_without_cut : Q.
  Proof.
    apply H1.
    intro H3; apply H0; apply H; assumption.
    apply H2.
    intro H3; apply H0; apply H; assumption.
  Qed.
End section_for_cut_example.

There maybe a better way to do this, but I think I captured the cut rule in the cut_example_without_cut.