proposition: Lemma applyIntersectIterate : forall (X : Set) (An : nat -> X -> Prop) (n : nat) (x : X), IntersectIterate An n x <-> forall (p:nat), le p n -> An p x.
proof: Proof. induction n. - split. intros. simpl in H. inversion H0. subst p. exact H. intros. simpl. apply H. apply Nat.le_refl. - split. + intros. apply Nat.le_succ_r in H0. destruct H0. apply IHn. apply H. exact H0. subst p. apply H. + intros. split. apply IHn. intros. apply H. apply (Nat.le_trans _ _ _ H0). apply le_S, Nat.le_refl. apply H. apply Nat.le_refl. Qed.
imports: Logic.ConstructiveEpsilon QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTPositivity