proposition: Lemma is_midpoint_id_2 : forall A B, Midpoint A B A -> A=B.
proof: Proof. intros. unfold Midpoint in *. spliter. apply cong_identity in H0. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR