proposition: Lemma rclo10_compose clo r: rclo10 (rclo10 clo) r <10= rclo10 clo r.
proof: Proof. intros. induction PR. - apply rclo10_base, IN. - apply rclo10_rclo. eapply rclo10_mon; [apply IN|apply H]. Qed.
imports: Program.Basics Paco(paco10 pacotac)