proposition: Lemma le_plus_distr : forall (A : Type)(m:M A), stable_plus m -> stable_inv m -> forall (f g:MF A), m (fplus f g) <= m f + m g.
proof: Proof. intros A m splus sinv; intros. apply Ole_trans with (m (fplus (fminus f (fesp f g)) g)). apply (fmonotonic m); intro x; unfold fminus,fesp,fplus,finv; intros; auto. rewrite (splus (fminus f (fesp f g)) g). Usimpl; auto. red; intro x; unfold fminus,fesp,finv; auto. Qed.
imports: ALEA(Uprop) ALEA(Utheory)