Elements of a doubled type in distinct pairs

In α ⊕ α, each label p has a partner p.swap with the same underlying element of α. Two labels that are neither equal nor partners have distinct underlying elements, so α has at least two elements.

Main results

• Sum.nontrivial_of_ne_of_ne_swap: if q ≠ p and q ≠ p.swap in α ⊕ α, then α is nontrivial.

theorem Sum.nontrivial_of_ne_of_ne_swap {α : Type u_1} {p q : α ⊕ α} (h : q ≠ p) (h' : q ≠ p.swap) : Nontrivial α

If two labels of α ⊕ α are neither equal nor partners under Sum.swap, then their underlying elements of α differ, so α is nontrivial.