proposition: Lemma rclo5_compose clo r: rclo5 (rclo5 clo) r <5= rclo5 clo r.
proof: Proof. intros. induction PR. - apply rclo5_base, IN. - apply rclo5_rclo. eapply rclo5_mon; [apply IN|apply H]. Qed.
imports: Program.Basics Paco(paco5 pacotac)