proposition: Lemma S_infty_nonzero : forall p : N_infty, S_infty p <> (nat_inj 0).
proof: Proof. intros. intro H. assert ((proj1_sig (S_infty p)) 0 = (proj1_sig (nat_inj 0)) 0). { rewrite H. reflexivity. } simpl in *. rewrite Nat.ltb_irrefl in H0. discriminate. Qed.
imports: Coq(FunctionalExtensionality Lia PeanoNat ProofIrrelevance ProofIrrelevanceFacts) ZornsLemma(FiniteTypes FunctionProperties) Coq(RelationClasses)