]; apply ex_intro; [| auto || auto ] (**)
qed.
(*
(* alternative proofs invoking nplus_gen_2 *)
variant nplus_gen_zero_3_alt: \forall p,q. (p + q == zero) \to
]; apply ex_intro; [| auto || auto ] (**)
qed.
(*
(* alternative proofs invoking nplus_gen_2 *)
variant nplus_gen_zero_3_alt: \forall p,q. (p + q == zero) \to