proposition: Lemma construction_uniqueness : forall Q A B C X Y, Q <> A -> Bet Q A X -> Cong A X B C -> Bet Q A Y -> Cong A Y B C -> X=Y.
proof: Proof. intros. assert (Cong A X A Y) by (apply cong_transitivity with B C; Cong). assert (Cong Q X Q Y) by (apply (l2_11 Q A X Q A Y);Cong). assert(OFSC Q A X Y Q A X X) by (unfold OFSC;repeat split;Cong). apply five_segment_with_def in H6; try assumption. apply cong_identity with X; Cong. Qed.
imports: GeoCoq.Tarski_dev.Definitions GeoCoq.Tactics.finish