proposition: Lemma sigma_fin_incl : forall f P (FP:finite P) Q (FQ:finite Q), (incl P Q) -> sigma_fin f FP <= sigma_fin f FQ.
proof: Proof. induction FP; simpl; intros; auto. destruct FQ; simpl; intros. case incl_add_empty with (a:=x) (P:=Q). apply incl_trans with Q0; auto. apply incl_trans with P; auto. case (decA x x0); intro. subst; Usimpl; auto. apply IHFP. apply incl_trans with (rem x0 P); auto. apply incl_add_rem; auto. apply incl_trans with (rem x0 Q0); auto. rewrite incl_rem_add_iff; auto. rewrite (sigma_fin_rem f FQ x). repeat norm_assoc_left. rewrite (Uplus_sym (f x0) (f x)). repeat norm_assoc_right. Usimpl. assert (H3:~(rem x Q1 x0)). unfold rem; intuition. assert (incl Q (add x0 (rem x Q1))). red; intros; case (e0 x1); clear e0; intuition. case (e x1); clear e; intuition. generalize (H x1); clear H; intuition. unfold add,rem in *; intuition. subst; intuition. case (decA x1 x0); intuition; subst; intuition. case (decA x1 x); intuition; subst; intuition. exact (IHFP (add x0 (rem x Q1)) (fin_eq_add H3 (finite_rem decA x FQ) (equiv_refl (add x0 (rem x Q1)))) H0). assert (P x). red in e; rewrite e; auto. assert (Q0 x);auto. assert (Q1 x);auto. case (e0 x); intuition. case H4; intuition. Qed.
imports: ALEA(Utheory) ALEA(Sets)