proposition: Lemma FIXP_comp : forall (D:cpo) (f g:D-c>D), g @_ f <= f @_ g -> f (FIXP D g) <= FIXP D g -> FIXP D (f @_ g) == FIXP D g.
proof: Proof. intros; apply Ole_antisym. apply FIXP_inv. rewrite fcont_comp_simpl. apply Ole_trans with (f (FIXP D g)); auto. apply FIXP_inv. assert (g (f (FIXP D (f @_ g))) <= f (g (FIXP D (f @_ g)))). apply (H (FIXP D (f @_ g))). case (FIXP_eq (f@_g)); intros. apply Ole_trans with (2:=H3). apply Ole_trans with (2:=H1). apply fcont_monotonic. apply FIXP_inv. rewrite fcont_comp_simpl. apply fcont_monotonic. apply Ole_trans with (1:=H1); auto. Qed.