proposition: Lemma l7_17 : forall P P' A B, Midpoint A P P' -> Midpoint B P P' -> A=B.
proof: Proof. intros. assert (Cong P B P' B). unfold Midpoint in *. spliter. Cong. assert (exists B', Midpoint A B B') by (apply symmetric_point_construction). induction H2. assert (Cong P' B P x) by eauto with midpoint cong. assert (Cong P B P x) by (apply cong_transitivity with P' B; Cong). assert (Cong P B P' x) by eauto with midpoint cong. assert (Cong P' B P' x) by (apply cong_transitivity with P x; Cong; apply cong_transitivity with P B; Cong). assert (Bet P B P') by (unfold Midpoint in *;spliter;assumption). assert (B=x) by (apply (l4_19 P P' B x);Between). subst x. apply l7_3. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR