proposition: Lemma l6_11_uniqueness : forall A B C R X Y, Out A X R -> Cong A X B C -> Out A Y R -> Cong A Y B C -> X=Y.
proof: Proof. unfold Out. intros. spliter. assert (Cong A X A Y) by CongR. induction H6; induction H4. apply l4_19 with A R; try assumption. apply l4_3 with A A; Between; Cong. assert (Bet A X Y) by eBetween. eapply between_cong; eauto. assert (Bet A Y X) by eBetween. apply sym_equal; apply between_cong with A; Cong. assert (Bet A X Y \/ Bet A Y X) by (eapply l5_1; eauto). induction H8. apply between_cong with A; assumption. apply sym_equal; apply between_cong with A; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le