proposition: Lemma applyUnionIterate : forall (X : Set) (An : nat -> X -> Prop) (n : nat) (x : X), UnionIterate An n x <-> exists (p:nat), le p n /\ An p x.
proof: Proof. induction n. - split. intros. exists O. split. reflexivity. apply H. intros. simpl. destruct H as [p [pneg pxp]]. inversion pneg. subst p. apply pxp. - split. + intros. simpl in H. destruct H. specialize (IHn x) as [H0 _]. destruct (H0 H). exists x0. split. apply (Nat.le_trans _ n). apply H1. apply le_S, Nat.le_refl. apply H1. exists (S n). split. apply Nat.le_refl. apply H. + intros. destruct H as [p [pxp H]]. apply Nat.le_succ_r in pxp. destruct pxp. left. specialize (IHn x) as [_ H3]. apply H3. exists p. split; assumption. subst p. right. exact H. Qed.
imports: Logic.ConstructiveEpsilon QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTPositivity