proposition: Lemma ZRECSPACE_def {A : Type'} : (@ZRECSPACE A) = (fun a : nat -> A -> Prop => forall ZRECSPACE' : (nat -> A -> Prop) -> Prop, (forall a' : nat -> A -> Prop, ((a' = (@ZBOT A)) \/ (exists c : nat, exists i : A, exists r : nat -> nat -> A -> Prop, (a' = (@ZCONSTR A c i r)) /\ (forall n : nat, ZRECSPACE' (r n)))) -> ZRECSPACE' a') -> ZRECSPACE' a).
proof: Proof. apply fun_ext; intro a. apply prop_ext. induction 1; intros a h; apply h. left. reflexivity. right. exists c. exists i. exists r. split. reflexivity. intro n. apply (H0 n a h). intro h. apply h. intros a' [e|[c [i [r [e j]]]]]; subst. apply ZRECSPACE0. apply ZRECSPACE1. exact j. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat