aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/Integer/Abstract/ZMaxMin.v
AgeCommit message (Collapse)Author
2010-02-09Numbers: properties of min/max with respect to 0,S,P,add,sub,mulletouzey
With these properties, we can kill Arith/MinMax, NArith/Nminmax, and leave ZArith/Zminmax as a compatibility file only. Now the instanciations NPeano.Nat, NBinary.N, ZBinary.Z, BigZ, BigN contains all theses facts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12718 85f007b7-540e-0410-9357-904b9bb8a0f7