proposition: Lemma is_midpoint_id : forall A B, Midpoint A A B -> A = B.
proof: Proof. intros. unfold Midpoint in H. spliter. treat_equalities;reflexivity. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR