proposition: Lemma FIXP_compn : forall (D:cpo) (f:D-c>D) (n:nat), FIXP D (fcont_compn f n) == FIXP D f.
proof: Proof. induction n; auto. simpl fcont_compn. apply FIXP_comp. apply fcont_compn_com. apply Ole_trans with (fcont_compn (D:=D) f n (FIXP D (fcont_compn (D:=D) f n))); auto. apply Ole_trans with (FIXP D (fcont_compn (D:=D) f n)); auto. Qed.