proposition: Lemma rtc_min A (R S : rel A) : PreOrder S -> R << S -> R# << S.
proof: Proof. intros S_PO RS. intros u v; revert u v; induction 1. fo. refl. trans y; hyp. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)