proposition: Lemma midpoint_distinct_2 : forall I A B, I<>A -> Midpoint I A B -> A<>B /\ I<>B.
proof: Proof. intros. assert (A<>B). intro. unfold Midpoint in *;spliter. treat_equalities. intuition. split. assumption. apply midpoint_distinct_1 in H0. intuition. intuition. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR