proposition: Lemma sym_preserve_diff : forall A B M A' B', A <> B -> Midpoint M A A' -> Midpoint M B B' -> A'<> B'.
proof: Proof. intros. intro. subst B'. assert (A = B). eapply l7_9. apply H0. assumption. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar