proposition: Lemma fixp_le_compat : forall (D:cpo) (f g : D-m>D), f<=g -> fixp f <= fixp g.
proof: Proof. intros; unfold fixp. apply lub_le_compat. intro n; induction n; simpl; auto. apply Ole_trans with (g (iter_ (D:=D) f n)); auto. Qed.