proposition: Lemma sams_suma__out213 : forall A B C D E F, SumA A B C D E F D E F -> SAMS A B C D E F -> Out B A C.
proof: Proof. intros A B C D E F HSuma HIsi. assert_diffs. apply (l11_21_a D E D). apply out_trivial; auto. apply sams_lea2_suma2__conga123 with D E F D E F D E F; Lea. exists F; repeat (split; CongA); Cop. apply col123__nos; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles