include "ground_2/notation/functions/successor_1.ma".
include "ground_2/notation/functions/predecessor_1.ma".
include "arithmetics/nat.ma".
-include "ground_2/lib/star.ma".
+include "ground_2/lib/relations.ma".
(* ARITHMETICAL PROPERTIES **************************************************)
(* Equations ****************************************************************)
+lemma plus_SO: ∀n. n + 1 = ⫯n.
+// qed.
+
lemma minus_plus_m_m_commutative: ∀n,m:nat. n = m + n - m.
// qed-.
lemma arith_i: ∀x,y,z. y < x → x+z-y-1 = x-y-1+z.
/2 width=1 by plus_minus/ qed-.
+lemma idempotent_max: ∀n:nat. n = (n ∨ n).
+#n normalize >le_to_leb_true //
+qed.
+
+lemma associative_max: associative … max.
+#x #y #z normalize
+@(leb_elim x y) normalize #Hxy
+@(leb_elim y z) normalize #Hyz //
+[1,2: >le_to_leb_true /2 width=3 by transitive_le/
+| >not_le_to_leb_false /4 width=3 by lt_to_not_le, not_le_to_lt, transitive_lt/
+ >not_le_to_leb_false //
+]
+qed.
+
(* Properties ***************************************************************)
lemma eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2).
(* Inversion & forward lemmas ***********************************************)
+lemma nat_split: ∀x. x = 0 ∨ ∃y. ⫯y = x.
+* /3 width=2 by ex_intro, or_introl, or_intror/
+qed-.
+
+lemma max_inv_O3: ∀x,y. (x ∨ y) = 0 → 0 = x ∧ 0 = y.
+/4 width=2 by le_maxr, le_maxl, le_n_O_to_eq, conj/
+qed-.
+
+lemma plus_inv_O3: ∀x,y. x + y = 0 → x = 0 ∧ y = 0.
+/2 width=1 by plus_le_0/ qed-.
+
lemma discr_plus_xy_y: ∀x,y. x + y = y → x = 0.
// qed-.