proposition: Lemma choice : (forall n : nat, {m : nat | P n m}) -> {d : nat -> nat | forall n : nat, P n (d n)}.
proof: Proof. intro H. exists (fun i : nat => proj1_sigT _ _ (H i)). apply (fun i : nat => proj2_sigT _ _ (H i)). Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)