proposition: Lemma cong3_bet_eq : forall A B C X, Bet A B C -> Cong_3 A B C A X C -> X = B.
proof: Proof. unfold Cong_3. intros. spliter. assert (IFSC A B C B A B C X) by (unfold IFSC;intuition). assert (Cong B B B X) by (apply (l4_2 _ _ _ _ _ _ _ _ H3)). treat_equalities. Between. Qed.
imports: GeoCoq.Tarski_dev.Ch03_bet GeoCoq.Tarski_dev.Tactics.CongR