Library Coq.Num.OppAxioms