Library Coq.Num.OppProps