proposition: Lemma construction_uniquenessT : forall Q A B C X Y, Q <> A -> BetG Q A X -> CongG A X B C -> BetG Q A Y -> CongG A Y B C -> X = Y.
proof: Proof. intros Q A B C X Y HDiff HBet1 HCong1 HBet2 HCong2. assert (HCong3 : CongG A X A Y) by (apply cong_inner_transitivityG with B C; auto). assert (HCong4 : CongG Q X Q Y) by (apply l2_11T with A A; auto; apply g2_1). assert (HCong5 : CongG X X X Y) by (apply five_segmentG with Q Q A A; auto; apply g2_1). apply g2_5 with X X; try apply g2_2; auto. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Tarski_dev.Ch05_bet_le