proposition: Lemma l7_9 : forall P Q A X, Midpoint A P X -> Midpoint A Q X -> P=Q.
proof: Proof. unfold Midpoint. intros. spliter. induction (eq_dec_points A X). treat_equalities;reflexivity. apply (construction_uniqueness X A X A);Cong;Between. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR