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