proposition: Lemma sams_lea2__sams : forall A B C D E F A' B' C' D' E' F', SAMS A' B' C' D' E' F' -> LeA A B C A' B' C' -> LeA D E F 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' Hisi HleaB HleaE. 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 _ _ _ _ _ _ A0); Between. apply (lea_trans D E F D' E' F'); auto. apply (lea_trans D' E' F' C' B' A'0). - apply (sams_chara A'); Between. - apply lea_comm. apply (l11_36 A B C A'); Between. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles