proposition: Lemma mid_two_sides : forall A B M X Y, Midpoint M A B -> ~ Col A B X -> Midpoint M X Y -> TS A B X Y.
proof: Proof. intros A B M X Y HM1 HNCol HM2. repeat split; Col. assert_diffs. assert (X<>Y) by (intro; treat_equalities; apply HNCol; Col). intro; apply HNCol; ColR. exists M; split; Col; Between. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar