proposition: Lemma midpoint_not_midpoint : forall I A B, A<>B -> Midpoint I A B -> ~ Midpoint B A I.
proof: Proof. intros. assert (I<>B). apply midpoint_distinct_1 in H0. tauto. assumption. apply midpoint_bet in H0. intro. apply midpoint_bet in H2. assert (I=B). apply between_symmetry in H0. apply between_symmetry in H2. eapply between_equality. apply H2. apply H0. intuition. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR