diff options
Diffstat (limited to 'theories/Numbers/Integer/Binary')
| -rw-r--r-- | theories/Numbers/Integer/Binary/ZBinary.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index 28a37abf85..5f87283940 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -63,6 +63,8 @@ Module Z Definition t := Z. Definition eqb := Zeq_bool. Definition zero := 0. +Definition one := 1. +Definition two := 2. Definition succ := Zsucc. Definition pred := Zpred. Definition add := Zplus. @@ -99,6 +101,16 @@ Definition sub_succ_r := Zminus_succ_r. Definition mul_0_l := Zmult_0_l. Definition mul_succ_l := Zmult_succ_l. +Lemma one_succ : 1 = Zsucc 0. +Proof. +reflexivity. +Qed. + +Lemma two_succ : 2 = Zsucc 1. +Proof. +reflexivity. +Qed. + (** Boolean Equality *) Definition eqb_eq x y := iff_sym (Zeq_is_eq_bool x y). |