proposition: Lemma compatible'5_companion clo (RES: compatible'5 clo): clo <6= cpn5 gf.
proof: Proof. assert (MON: monotone5 gf'5). { econstructor. apply LE, IN. eapply gf_mon, LE. apply IN. } assert (CPN: clo <6= cpn5 gf'5). { intros. econstructor. apply RES. apply PR. } intros. apply CPN in PR. econstructor; [|apply PR]. econstructor; [apply cpn5_mon|]; intros. assert (PR1: cpn5 gf'5 (gf r) <5= cpn5 gf'5 (gf'5 (cpn5 gf r))). { intros. eapply cpn5_mon. apply PR1. intros. assert (TMP: gf (cpn5 gf r) <5= (cpn5 gf r /5\ gf (cpn5 gf r))). { split; [apply cpn5_step; [apply gf_mon|]|]; assumption. } apply TMP. eapply gf_mon. apply PR2. intros. apply cpn5_base; assumption. } apply PR1 in PR0. clear PR1. eapply compat5_compat with (gf:=gf'5) in PR0; [|apply cpn5_compat, MON]. eapply gf_mon; [apply PR0|]. intros. eapply cpn5_cpn; [apply MON|]. eapply cpn5_mon; [apply PR1|]. intros. econstructor; [|apply PR2]. apply compat5_compatible', cpn5_compat, gf_mon. Qed.
imports: Program.Basics Paco(paco5 pacotac)