proposition: Lemma sigma_inv : forall (f g : nat -> U) (n:nat), (retract f n) -> [1-] (sigma (fun k => f k * g k) n) == (sigma (fun k => f k * [1-] (g k)) n) + [1-] (sigma f n).
proof: Proof. intros; induction n; repeat rewrite sigma_S; auto. apply Uplus_eq_simpl_right with ((f n) * (g n)). rewrite (Uinv_inv (f n * g n + sigma (fun k : nat => f k * g k) n));auto. apply Uinv_le_perm_right. rewrite (Udistr_inv_left (f n) (g n)). repeat norm_assoc_right; apply Uplus_le_compat_right. apply Ole_trans with (sigma f n + [1-] (f n + sigma f n)); auto. assert (sigma f n <= [1-] (f n)). apply Uinv_le_perm_right; auto. rewrite <- (Uinv_plus_right _ _ H0); auto. assert (sigma (fun k : nat => f k * g k) n <= [1-] (f n * g n)). apply Ole_trans with (sigma f n); auto. apply Ole_trans with ([1-] (f n)); auto. rewrite (Uinv_plus_left _ _ H0). apply Oeq_trans with (1:=IHn (retract_pred H)). rewrite (Uplus_sym (f n * [1-] (g n)) (sigma (fun k : nat => f k * [1-] (g k)) n)). repeat norm_assoc_right; apply Uplus_eq_compat_right. rewrite (Uplus_sym ([1-] (f n + sigma f n)) (f n * g n)). repeat norm_assoc_left. assert ([1-] (g n) <= [1-] (g n)); auto. rewrite <- (Udistr_plus_left (f n) _ _ H1). rewrite (Uinv_opp_left (g n)). rewrite (Umult_one_right (f n)); auto. rewrite (Uplus_sym (f n) ([1-] (f n + sigma f n))). apply Oeq_sym; apply Uinv_plus_left; auto. Qed.
imports: ALEA(Utheory)