proposition: Lemma sams2_suma2__conga : forall A B C D E F A' B' C', SAMS A B C A B C -> SumA A B C A B C D E F -> SAMS A' B' C' A' B' C' -> SumA A' B' C' A' B' C' D E F -> CongA A B C A' B' C'.
proof: Proof. intros A B C D E F A' B' C' HIsi HSuma HIsi' HSuma'. assert_diffs. destruct (lea_total A B C A' B' C'); trivial; [|apply conga_sym]; eapply sams_lea2_suma2__conga123; eauto. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles