proposition: Lemma okup_fixrule_glb : forall p : A -> natO -m> UI, (forall (i:nat) (f:A->Distr B), (upfun (fun x => p x i) f q) -> upfun (fun x => p x (S i)) (fun x => F f x) q) -> upfun (fun x => glb (p x)) (Mfix F) q.
proof: Proof. red; intros p Hrec x. assert (forall n:nat, (upfun (fun x => (p x n)) (fun x => (Miter F n x)) q)). induction n; simpl; auto. red; red; intros; auto. red; intros. unfold Mfix, fixp; simpl. apply lub_glb_le; auto. intro n; exact (H n x). Qed.
imports: ALEA(Probas) ALEA(Utheory)