proposition: Lemma rclo11_compose clo r: rclo11 (rclo11 clo) r <11= rclo11 clo r.
proof: Proof. intros. induction PR. - apply rclo11_base, IN. - apply rclo11_rclo. eapply rclo11_mon; [apply IN|apply H]. Qed.
imports: Program.Basics Paco(paco11 pacotac)