proposition: Lemma Exercise6_33t: E6_33_N_prop N E6_33_z.
proof: Proof. set p := (fun z => E6_33_N_prop (P z) (Q z)). have h: (exists y, p y). move: Exercise6_33s =>[n [z etc]]; exists (J n z). by rewrite /p; aw. by move: (choose_pr h). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)