proposition: Lemma NUMSND1_NUMPAIR x y : NUMSND1 (NUMPAIR x y) = y.
proof: Proof. destruct (INJ_INVERSE2 _ NUMPAIR_INJ) as [fst [snd h]]. assert (i : exists x, NUMSND1_pred x). exists snd. unfold NUMSND1_pred. intros x' y'. rewrite NUMFST_NUMPAIR. destruct (h x' y') as [h1 h2]. auto. generalize (ε_spec i). fold NUMSND1. unfold NUMSND1_pred. intro j. destruct (j x y) as [j1 j2]. exact j2. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat