proposition: Lemma rclo8_compose clo r: rclo8 (rclo8 clo) r <8= rclo8 clo r.
proof: Proof. intros. induction PR. - apply rclo8_base, IN. - apply rclo8_rclo. eapply rclo8_mon; [apply IN|apply H]. Qed.
imports: Program.Basics Paco(paco8 pacotac)