proposition: Lemma le_esp_distr : forall (A : Type) (m:M A), stable_plus m -> stable_inv m -> le_esp m.
proof: Proof. intros A m splus sinv; unfold le_esp,fesp,Uesp; intros. apply Ole_trans with (m (finv (fplus (finv f) (finv g)))). 2:auto. rewrite inv_minus_distr; trivial. apply Ole_trans with (m (fone A) - (m (finv f) + m (finv g))). 2:auto. apply Ole_trans with (m f - [1-] m g) ; repeat Usimpl. auto. rewrite inv_minus_distr; trivial. apply Ole_trans with (m f - m (finv g)) ; repeat Usimpl. apply Uminus_le_compat_right; trivial. rewrite <- Uminus_assoc_left. rewrite Uminus_assoc_right; repeat Usimpl; auto. Qed.
imports: ALEA(Uprop) ALEA(Utheory)