fact: Definition proj1_sigT (A : Type) (P : A -> CProp) (e : sigT P) := match e with | existT _ a b => a end.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)