proposition: Lemma FIXP_comp_com : forall (D:cpo) (f g:D-c>D), g @_ f <= f @_ g-> FIXP D g <= f (FIXP D g).
proof: Proof. intros; apply FIXP_inv. apply Ole_trans with (f (g (FIXP D g))). apply (fcont_le_elim H (FIXP D g)). apply fcont_monotonic. case (FIXP_eq g); trivial. Qed.