proposition: Lemma clos_trans_stepr A (R : relation A) (x y z : A) : R y z -> clos_trans A R x y -> clos_trans A R x z.
proof: Proof. intros Hyz Hxy. exact (t_trans _ _ x y z Hxy (t_step _ _ _ _ Hyz)). Defined.
imports: Coq(Wf_nat Relations) Coq(Wellfounded Relation_Definitions) Coq(Relation_Operators Lexicographic_Product Wf_nat) Equations(Init Signature) Equations.CoreTactics Equations.Prop.Classes Equations.Prop.EqDec Equations.Prop.DepElim Equations.Prop.Constants