proposition: Lemma bet_suma2__or_conga : forall A B C D E F A' B' C' A0, A0 <> B -> Bet A B A0 -> 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' \/ CongA A0 B C A' B' C'.
proof: Proof. intros A B C D E F A' B' C' A0 HBA0 HBet HSuma. revert A' B' C'. assert (Haux : forall A' B' C', Acute A' B' C' -> SumA A' B' C' A' B' C' D E F -> CongA A B C A' B' C' \/ CongA A0 B C A' B' C'). { intros A' B' C' HAcute' HSuma'. assert_diffs. destruct (angle_partition A B C) as [HAcute|[HPer|HObtuse]]; auto. - left; apply acute2_suma2__conga with D E F; auto. - exfalso. apply (acute_suma__nbet A' B' C' D E F); [..|apply (per2_suma__bet A B C A B C)]; assumption. - right; apply acute2_suma2__conga with D E F; auto. apply (bet_obtuse__acute A); auto. apply bet2_suma__suma with A A; auto. } intros A' B' C' HSuma'. assert_diffs. destruct (angle_partition A' B' C') as [HAcute|[HPer|HObtuse]]; auto. - left. apply l11_16; auto. apply bet_suma__per with D E F; [apply (per2_suma__bet A' B' C' A' B' C')|]; assumption. - destruct (segment_construction A' B' A' B') as [A0' []]. assert_diffs. destruct (Haux A0' B' C'). apply (bet_obtuse__acute A'); auto. apply bet2_suma__suma with A' A'; auto. right; apply l11_13 with A A0'; Between. left; apply l11_13 with A0 A0'; Between. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles