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