proposition: Corollary paco5_mult: forall r, paco5 gf (paco5 gf r) <5= paco5 gf r.
proof: Proof. intros; eapply paco5_mult_strong, paco5_mon; [apply PR|..]; intros; left; assumption. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)