proposition: Lemma midpoint_distinct_1 : forall I A B, A<>B -> Midpoint I A B -> I<>A /\ I<>B.
proof: Proof. intros. split. intro. subst. unfold Midpoint in *. decompose [and] H0. treat_equalities. intuition. intro;subst. unfold Midpoint in *. decompose [and] H0. treat_equalities. intuition. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR