proposition: Lemma trans_intro A (R : rel A) : R @ R << R <-> Transitive R.
proof: Proof. split. unfold Transitive. intros. apply H. exists y. intuition. intros h x z [y [xy yz]]. apply (h _ _ _ xy yz). Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)