proposition: Lemma inv_minus_distr : forall (A:Type) (m:M A), stable_plus m -> stable_inv m -> forall (f : MF A), m (finv f) == m (fone A) - m f.
proof: Proof. intros A m splus sinv; intros. apply Oeq_trans with (m (fminus (fone A) f)); auto. apply (fmon_stable m). simpl; apply ford_eq_intro; intro x; unfold fminus,finv,fone,fplus; intros; auto. Qed.
imports: ALEA(Uprop) ALEA(Utheory)