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 **************************************************)
(* 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-.