proposition: Lemma muF_le_term_minus : forall f, f <= pterm -> muFqinv (fminus pterm f) <= fminus pterm f -> forall x, f x <= mu (Mfix F x) (q x).
proof: Proof. intros; apply Ole_trans with ((f x + [1-]pterm x) & pterm x). red in H; rewrite Uplus_inv_esp_simpl; auto. apply muF_le_term with (f:=fun y => f y + [1-]pterm y); auto. apply Ole_trans with (muFqinv (fminus pterm f)). apply (fmonotonic muFqinv); unfold fminus, finv; intro y. apply Uinv_le_perm_left; auto. apply Ole_trans with (fminus pterm f); auto. unfold fminus, Uminus, finv; intro y; auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)