proposition: Lemma star_stable_mult : forall (A B:Type) (m:M A) (F:A -> M B), stable_mult m -> (forall a:A, stable_mult (F a)) -> stable_mult (star m F).
proof: Proof. unfold stable_mult in |- *; intros. unfold star in |- *; simpl. apply Oeq_trans with (m (fmult k (fun x:A => F x f))); trivial. apply (fmon_stable m). simpl; apply ford_eq_intro; intro. unfold fmult at 2 in |- *; trivial. Qed.
imports: ALEA(Uprop) ALEA(Utheory)