proposition: Lemma midpoint_opp: forall O E E' A B, Ar2 O E E' O A B -> Midpoint O A B -> Opp O E E' A B.
proof: Proof. intros. unfold Ar2. unfold Ar2 in H. spliter. clear H1. unfold Midpoint in H0. spliter. induction (eq_dec_points A B). subst B. apply between_identity in H0. subst A. apply opp0; auto. unfold Opp. apply cong_sum; auto. unfold Ar2. repeat split; Col. Cong. Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg