proposition: Lemma midpoint_dec : forall I A B, Midpoint I A B \/ ~ Midpoint I A B.
proof: Proof. intros. unfold Midpoint. elim (bet_dec A I B);intro; elim (cong_dec A I I B);intro; tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR