diff options
Diffstat (limited to 'theories/ZArith/BinIntDef.v')
| -rw-r--r-- | theories/ZArith/BinIntDef.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v index ee9051ff8..d96d20fbb 100644 --- a/theories/ZArith/BinIntDef.v +++ b/theories/ZArith/BinIntDef.v @@ -132,6 +132,15 @@ Definition pow x y := Infix "^" := pow : Z_scope. +(** ** Square *) + +Definition square x := + match x with + | 0 => 0 + | Zpos p => Zpos (Pos.square p) + | Zneg p => Zpos (Pos.square p) + end. + (** ** Comparison *) Definition compare x y := |