proposition: Lemma N_infty_false_eq_nat_inj' : forall p : N_infty, forall n : nat, (proj1_sig p) n = false -> { n' : nat | N_equiv p (nat_inj n') }.
proof: Proof. intros. destruct (N_infty_false_minimal p n H) as [n' []]. exists n'. red. intros. simpl. destruct (n0 <? n') eqn:?. - apply H1. apply Nat.ltb_lt. assumption. - apply N_infty_false_le with n'; auto. apply Nat.ltb_ge in Heqb. assumption. Qed.
imports: Coq(FunctionalExtensionality Lia PeanoNat ProofIrrelevance ProofIrrelevanceFacts) ZornsLemma(FiniteTypes FunctionProperties) Coq(RelationClasses)