proposition: Lemma midpoint_out : forall A B C, A <> C -> Midpoint B A C -> Out A B C.
proof: Proof. intros. repeat split. apply midpoint_distinct_1 in H0; spliter; auto. auto. left. apply midpoint_bet. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR