proposition: Lemma NUMSND0_NUMPAIR x y : NUMSND0 (NUMPAIR x y) = y.
proof: Proof. destruct (INJ_INVERSE2 _ NUMPAIR_INJ) as [fst [snd h]]. assert (i : exists x, NUMSND0_pred x). exists snd. exists fst. assumption. generalize (ε_spec i). fold NUMSND0. unfold NUMSND0_pred. intros [fst' h']. destruct (h' x y) as [j k]. assumption. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat