proposition: Lemma star_stable_plus : forall (A B:Type) (m:M A) (F:A -> M B), stable_plus m -> (forall a:A, forall f g, fplusok f g -> (F a f) <= Uinv (F a g)) -> (forall a:A, stable_plus (F a)) -> stable_plus (star m F).
proof: Proof. unfold stable_plus in |- *; intros. unfold star in |- *; simpl. apply Oeq_trans with (m (fplus (fun x:A => F x f) (fun x:A => F x g))); trivial. apply (fmon_stable m). simpl; apply ford_eq_intro; intros x; apply (H1 x f g H2). apply H. red; intro x; unfold finv; intros; auto. Qed.
imports: ALEA(Uprop) ALEA(Utheory)