This project follows closely Schwabenhaeuser.
See set.mm#2983:
We do have all 3 segment versions of CPCTC, namely
cgr3simp1
,cgr3simp2
, andcgr3simp3
; we're just missing two of the CPCTC angle forms.SAS is already proven in
tgsas1
andtgsas
. ASA is proven intgasa1
andtgasa
. We don't actually have a proof of AAS (Angle-Angle-Side), Theorem 11.50 of [Schwabhauser] p. 108, we just have a placeholder.