ordConnected_C1

lemma ordConnected_C1 : OrdConnected (ℭ₁ k n j : Set (𝔓 X)) := by  rw [ordConnected_def]; intro p mp p'' mp'' p' mp'  have mp'₁ : p' ∈ ℭ (X := X) k n := mem_of_mem_of_subset mp'    (ordConnected_C.out (mem_of_mem_of_subset mp ℭ₁_subset_ℭ)      (mem_of_mem_of_subset mp'' ℭ₁_subset_ℭ))  simp_rw [ℭ₁, mem_sdiff, preℭ₁, mem_setOf, not_and, not_le] at mp mp'' ⊢  simp_rw [mp.1.1, true_and, true_implies] at mp  simp_rw [mp'₁, true_and, true_implies]  simp_rw [mp''.1.1, true_and, true_implies] at mp''  constructor  · refine mp''.1.trans (Finset.card_le_card fun b mb ↦ ?_)    simp_rw [Finset.mem_filter_univ, 𝔅, mem_setOf] at mb ⊢    have h100 := wiggle_order_11_10 (n := 100) mp'.2 (C5_3_3_le (X := X).trans (by norm_num))    exact ⟨mb.1, h100.trans mb.2⟩  · refine (Finset.card_le_card fun b mb ↦ ?_).trans_lt mp.2    simp_rw [Finset.mem_filter_univ, 𝔅, mem_setOf] at mb ⊢    have h100 := wiggle_order_11_10 (n := 100) mp'.1 (C5_3_3_le (X := X).trans (by norm_num))    exact ⟨mb.1, h100.trans mb.2⟩