proposition: Lemma sams_suma__lea456789 : forall A B C D E F G H I, SumA A B C D E F G H I -> SAMS A B C D E F -> LeA D E F G H I.
proof: Proof. intros A B C D E F G H I Hsuma Hisi. apply (sams_suma__lea123789 D E F A B C G H I); SumA. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles