Lemma leastfixedpoint_isfixedpoint {D : dcpowithbottom} : ∏ (f : D --> D), (pr1 f) (pr1 μ f) = pr1 μ f. Proof. intro f. unfold leastfixedpoint; cbn. apply isantisymm_posetRelation. - set (isdirec := pointwisefamily_isdirected iter' (iter'_isdirected D) f). eapply dcpomorphism_preserveslub. + exact isdirec. + apply pointwiselub_islubpointwise. + intro n. simpl. eapply (istrans_posetRelation _ _ (pointwisefamily iter' f (S n)) _). * apply isrefl_posetRelation. * apply pointwiselub_islubpointwise. - eapply (islub_isleast). + apply pointwiselub_islubpointwise. + intro n. induction n as [ | m IH]. * apply dcpowithbottom_isMinimal. * unfold pointwisefamily; simpl. apply dcpomorphism_preservesorder. eapply istrans_posetRelation. -- use iter'_increases. ++ exact (S m). ++ apply natlehnsn. -- exact (islub_isupperbound _ (pointwiselub_islubpointwise iter' (iter'_isdirected D) f) (S m)). Qed.
Require Import UniMath.Foundations.All.