proposition: Lemma l7_9_bis : forall P Q A X, Midpoint A P X -> Midpoint A X Q -> P=Q.
proof: Proof. intros; apply l7_9 with A X; unfold Midpoint in *; split; spliter; Cong; Between. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR