proposition: Lemma muF_eq : forall f, muFq f <= f -> muFqinv (finv f) <= finv f -> forall x, pterm x == 1 -> mu (Mfix F x) (q x) == f x.
proof: Proof. intros; apply Ole_antisym. apply muF_le with (muF:=muFq); auto. apply Ole_trans with (f x & pterm x). rewrite H1; auto. apply muF_le_term; auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)