Symmetry lemmas for the permutation tactics. These rewrite the geometric primitives (area, colinear, triangle, length, angle, SameSide, diffside, para) under permutations of their point arguments, and serve as the building blocks for the perm/perma/linperm tactics defined in PermTactics.

theorem SyntheticEuclid4.ar132 [i : IncidenceGeometry] {a b c : IncidenceGeometry.Point} : IncidenceGeometry.area a b c = IncidenceGeometry.area a c b

theorem SyntheticEuclid4.ar312 [i : IncidenceGeometry] {a b c : IncidenceGeometry.Point} : IncidenceGeometry.area a b c = IncidenceGeometry.area c a b

theorem SyntheticEuclid4.ar231 [i : IncidenceGeometry] {a b c : IncidenceGeometry.Point} : IncidenceGeometry.area a b c = IncidenceGeometry.area b c a

theorem SyntheticEuclid4.ar213 [i : IncidenceGeometry] {a b c : IncidenceGeometry.Point} : IncidenceGeometry.area a b c = IncidenceGeometry.area b a c

theorem SyntheticEuclid4.ar321 [i : IncidenceGeometry] {a b c : IncidenceGeometry.Point} : IncidenceGeometry.area a b c = IncidenceGeometry.area c b a

theorem SyntheticEuclid4.col213 [i : IncidenceGeometry] {a b c : IncidenceGeometry.Point} : colinear a b c ↔ colinear b a c

theorem SyntheticEuclid4.col231 [i : IncidenceGeometry] {a b c : IncidenceGeometry.Point} : colinear a b c ↔ colinear b c a

theorem SyntheticEuclid4.col132 [i : IncidenceGeometry] {a b c : IncidenceGeometry.Point} : colinear a b c ↔ colinear a c b

theorem SyntheticEuclid4.col312 [i : IncidenceGeometry] {a b c : IncidenceGeometry.Point} : colinear a b c ↔ colinear c a b

theorem SyntheticEuclid4.col321 [i : IncidenceGeometry] {a b c : IncidenceGeometry.Point} : colinear a b c ↔ colinear c b a

theorem SyntheticEuclid4.tr132 [i : IncidenceGeometry] {a b c : IncidenceGeometry.Point} : triangle a b c ↔ triangle a c b

theorem SyntheticEuclid4.tr213 [i : IncidenceGeometry] {a b c : IncidenceGeometry.Point} : triangle a b c ↔ triangle b a c

theorem SyntheticEuclid4.tr231 [i : IncidenceGeometry] {a b c : IncidenceGeometry.Point} : triangle a b c ↔ triangle b c a

theorem SyntheticEuclid4.tr312 [i : IncidenceGeometry] {a b c : IncidenceGeometry.Point} : triangle a b c ↔ triangle c a b

theorem SyntheticEuclid4.tr321 [i : IncidenceGeometry] {a b c : IncidenceGeometry.Point} : triangle a b c ↔ triangle c b a

theorem SyntheticEuclid4.ss21 [i : IncidenceGeometry] {a b : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} : IncidenceGeometry.SameSide a b L ↔ IncidenceGeometry.SameSide b a L

theorem SyntheticEuclid4.ds21 [i : IncidenceGeometry] {a b : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} : diffside a b L ↔ diffside b a L

theorem SyntheticEuclid4.para21 [i : IncidenceGeometry] {L M : IncidenceGeometry.Line} : para L M ↔ para M L