proposition: Lemma N_infty_false_le : forall p : N_infty, forall n : nat, (proj1_sig p) n = false -> forall m : nat, n <= m -> (proj1_sig p) m = false.
proof: Proof. intros. destruct (proj1_sig p m) eqn:?; auto. exfalso. apply (proj2_sig p m) with n in Heqb. - rewrite Heqb in H; discriminate. - induction H0. + rewrite Heqb in H; discriminate. + apply Nat.lt_lt_succ_r. apply IHle. apply (proj2_sig p (S m)); auto. Qed.
imports: Coq(FunctionalExtensionality Lia PeanoNat ProofIrrelevance ProofIrrelevanceFacts) ZornsLemma(FiniteTypes FunctionProperties) Coq(RelationClasses)