proposition: Lemma ltb_0_r (n : nat) : n <? 0 = false.
proof: Proof. induction n; auto. Qed.
imports: Coq(FunctionalExtensionality Lia PeanoNat ProofIrrelevance ProofIrrelevanceFacts) ZornsLemma(FiniteTypes FunctionProperties) Coq(RelationClasses)