proposition: Lemma star_le_plus : forall (A B:Type) (m:M A) (F:A -> M B), le_plus m -> (forall a:A, forall f g, fplusok f g -> (F a f) <= Uinv (F a g)) -> (forall a:A, le_plus (F a)) -> le_plus (star m F).
proof: Proof. unfold le_plus in |- *; intros. unfold star in |- *; simpl. apply Ole_trans with (m (fplus (fun x:A => F x f) (fun x:A => F x g))); trivial. apply H. red;intro x; unfold finv; intros; auto. apply (fmonotonic m). simpl; unfold fplus at 1; auto. Qed.
imports: ALEA(Uprop) ALEA(Utheory)