proposition: Lemma tc_min A (R S : rel A) : R << S -> Transitive S -> R! << S.
proof: Proof. intros RS Strans. intros x y. induction 1. apply RS. hyp. trans y; hyp. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)