proposition: Lemma symmetry_preserves_midpoint : forall A B C D E F Z, Midpoint Z A D -> Midpoint Z B E -> Midpoint Z C F -> Midpoint B A C -> Midpoint E D F.
proof: Proof. intros. unfold Midpoint. unfold Midpoint in H2. spliter. split. eapply l7_15;eauto. eapply l7_16;eauto. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR