proposition: Lemma Mid_perm : forall A B C, Midpoint A B C -> Midpoint A B C /\ Midpoint A C B.
proof: Proof. unfold Midpoint. intros. spliter. repeat split; Between; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR