proposition: Lemma sams_sym : forall A B C D E F, SAMS A B C D E F -> SAMS D E F A B C.
proof: Proof. intros A B C D E F Hisi. assert(A<>B/\B<>C/\D<>E/\E<>F) by (apply sams_distincts; auto). spliter. assert(HD' : exists D', Midpoint E D D') by apply symmetric_point_construction. destruct HD' as [D']. assert(HA' : exists A', Midpoint B A A') by apply symmetric_point_construction. destruct HA' as [A']. assert_diffs. apply (sams_chara D E F A B C D'); Between. apply lea_right_comm. apply (l11_36 D _ _ A'); Between. apply lea_right_comm. apply (sams_chara A); Between. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles