proposition: Lemma bet__trisuma : forall A B C D E F, Bet D E F -> A <> B -> B <> C -> A <> C -> D <> E -> E <> F -> TriSumA A B C D E F.
proof: Proof. intros A B C D E F HBet; intros. destruct (ex_trisuma A B C) as [P [Q [R HTri]]]; auto. apply conga_trisuma__trisuma with P Q R; trivial. assert (Hd := HTri). apply trisuma_distincts in Hd; spliter. apply conga_line; auto. apply (trisuma__bet A B C); trivial. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec