proposition: Lemma clos_trans_inv {A} R (x y z : A) : clos_trans A R y z → clos_trans A R x y → clos_trans A R x z.
proof: Proof. eauto using t_trans. Qed.
imports: Equations(Equations) Lia List Utf8 Arith Lia Relations Setoid Arith Wf_nat