proposition: Lemma rclo7_compose clo r: rclo7 (rclo7 clo) r <7= rclo7 clo r.
proof: Proof. intros. induction PR. - apply rclo7_base, IN. - apply rclo7_rclo. eapply rclo7_mon; [apply IN|apply H]. Qed.
imports: Program.Basics Paco(paco7 pacotac)