proposition: Lemma clos_rt_t : forall x y z, clos_refl_trans R x y -> clos_trans R y z -> clos_trans R x z.
proof: Proof. induction 1 as [b d H1|b|a b d H1 H2 IH1 IH2]; auto. intro H. apply (t_trans _ _ _ d); auto. constructor. auto. Qed.
imports: Relation_Definitions Relation_Operators