proposition: Lemma stable_minus_distr : forall (A:Type) (m:M A), stable_plus m -> stable_inv m -> forall (f g : MF A), g <= f -> m (fminus f g) == m f - m g.
proof: Proof. intros A m splus sinv; intros. assert (m g <= m f); auto. assert (fminus f g <= finv g). intros; intro x; unfold fminus,Uminus,fplus, finv; auto. rewrite (fmon_stable m (x:=f) (y:=fplus (fminus f g) g)). rewrite (splus (fminus f g) g); auto. rewrite Uplus_minus_simpl_right; auto. apply Uinv_le_perm_right. apply Ole_trans with (m (finv g)); auto. simpl; apply ford_eq_intro; intro x; unfold fplus,fminus; auto. Qed.
imports: ALEA(Uprop) ALEA(Utheory)