proposition: Lemma conga2_sams__sams : forall A B C D E F A' B' C' D' E' F', CongA A B C A' B' C' -> CongA D E F D' E' F' -> SAMS A B C D E F -> SAMS A' B' C' D' E' F'.
proof: Proof. intros A B C D E F A' B' C' D' E' F' HCongaB HCongaE Hisi. assert(HA0 : exists A0, Midpoint B A A0) by apply symmetric_point_construction. destruct HA0 as [A0]. assert(HA'0 : exists A'0, Midpoint B' A' A'0) by apply symmetric_point_construction. destruct HA'0 as [A'0]. assert_diffs. apply (sams_chara _ _ _ _ _ _ A'0); Between. apply (l11_30 D E F C B A0); try (apply (sams_chara A)); Between. apply conga_comm. apply (l11_13 A B C A'); Between. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles