proposition: Fact nat_inj_inj : injective nat_inj.
proof: Proof. red; intros. unfold nat_inj in *. apply proj1_sig_eq in H. simpl in *. pose (Hx := (fun m => m <? x) x = (fun m => m <? y) x). pose (Hy := (fun m => m <? x) y = (fun m => m <? y) y). assert Hx. { red. rewrite H. reflexivity. } assert Hy. { red. rewrite H. reflexivity. } simpl in *. red in H0, H1. rewrite Nat.ltb_irrefl in *. symmetry in H0. apply Nat.ltb_ge in H0. apply Nat.ltb_ge in H1. apply Nat.le_antisymm; assumption. Qed.
imports: Coq(FunctionalExtensionality Lia PeanoNat ProofIrrelevance ProofIrrelevanceFacts) ZornsLemma(FiniteTypes FunctionProperties) Coq(RelationClasses)