proposition: Lemma sigma_fin_inv : forall (f g : A -> U)(P:A->Prop)(FP:finite P), retract_fin P f -> [1-] sigma_fin (fun k => f k * g k) FP == sigma_fin (fun k => f k * [1-] g k) FP + [1-] sigma_fin f FP.
proof: Proof. induction FP; simpl. repeat Usimpl; auto. intro. assert (incl Q P). apply incl_trans with (add x Q); auto. assert (retract_fin Q f). apply retract_fin_incl with P; auto. assert (px:P x). case (e x); intuition. apply Uplus_eq_simpl_right with ((f x) * (g x)). repeat Usimpl; auto. apply Uinv_le_perm_right. rewrite (Udistr_inv_left (f x) (g x)). repeat norm_assoc_right; apply Uplus_le_compat_right. apply Ole_trans with (sigma_fin f FP + [1-] (f x + sigma_fin f FP)); repeat Usimpl. apply (sigma_fin_prod_maj f (fun k => [1-](g k)) FP). assert (sigma_fin f FP <= [1-] (f x)). apply Uinv_le_perm_right; auto. rewrite <- (Uinv_plus_right _ _ H2); auto. assert (sigma_fin (fun k => f k * g k) FP <= [1-] (f x * g x)). apply Ole_trans with (sigma_fin f FP); auto. apply Ole_trans with ([1-] (f x)); auto. apply Uinv_le_perm_right; auto. rewrite (Uinv_plus_left _ _ H2). apply Oeq_trans with (1:=IHFP H1). rewrite (Uplus_sym (f x * [1-] (g x)) (sigma_fin (fun k => f k * [1-] (g k)) FP)). repeat norm_assoc_right;apply Uplus_eq_compat_right. setoid_rewrite (Uplus_sym ([1-] (f x + sigma_fin f FP)) (f x * g x)). repeat norm_assoc_left. assert ([1-] (g x) <= [1-] (g x)); auto. rewrite <- (Udistr_plus_left (f x) _ _ H3). rewrite (Uinv_opp_left (g x)). rewrite (Umult_one_right (f x)); auto. rewrite (Uplus_sym (f x) ([1-] (f x + sigma_fin f FP))). apply Oeq_sym; apply Uinv_plus_left; auto. apply Uinv_le_perm_right; auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)