feat(set_theory/principal): If a isn't additive principal, it's the…

… sum of two smaller ordinals (#12664)

src/set_theory/principal.lean

@@ -148,6 +148,26 @@ begin
     exact (add_is_normal a).strict_mono hbo }
 end
 
+theorem exists_lt_add_of_not_principal_add {a} (ha : ¬ principal (+) a) :
+  ∃ (b c) (hb : b < a) (hc : c < a), b + c = a :=
+begin
+  unfold principal at ha,
+  push_neg at ha,
+  rcases ha with ⟨b, c, hb, hc, H⟩,
+  refine ⟨b, _, hb, lt_of_le_of_ne (sub_le_self a b) (λ hab, _),
+    ordinal.add_sub_cancel_of_le hb.le⟩,
+  rw [←sub_le, hab] at H,
+  exact H.not_lt hc
+end
+
+theorem principal_add_iff_add_lt_ne_self {a} :
+  principal (+) a ↔ ∀ ⦃b c⦄, b < a → c < a → b + c ≠ a :=
+⟨λ ha b c hb hc, (ha hb hc).ne, λ H, begin
+  by_contra' ha,
+  rcases exists_lt_add_of_not_principal_add ha with ⟨b, c, hb, hc, rfl⟩,
+  exact (H hb hc).irrefl
+end⟩
+
 theorem add_omega {a : ordinal} (h : a < omega) : a + omega = omega :=
 begin
   rcases lt_omega.1 h with ⟨n, rfl⟩,