proposition: Lemma suma2__or_conga_suppa : forall A B C A' B' C' D E F , SumA A B C A B C D E F -> SumA A' B' C' A' B' C' D E F -> CongA A B C A' B' C' \/ SuppA A B C A' B' C'.
proof: Proof. intros A B C A' B' C' D E F HSuma HSuma'. destruct (segment_construction A B A B) as [A0 []]. assert_diffs. destruct (bet_suma2__or_conga A B C D E F A' B' C' A0); auto. right. split; auto. exists A0; split; CongA. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles