proposition: Lemma mid2_orth_at2__cong : forall A B C X Y P Q P' Q', Orth_at X A B C X P -> Orth_at Y A B C Y Q -> Midpoint X P P' -> Midpoint Y Q Q' -> Cong P Q P' Q'.
proof: Proof. intros A B C X Y P Q P' Q' HX1 HY1 HX2 HY2. assert (HX3 := HX1). destruct HX3 as [HNCol [HXP [HCop1 [_ HX3]]]]. assert (HY3 := HY1). destruct HY3 as [_ [HYQ [HCop2 [_ HY3]]]]. destruct (midpoint_existence X Y) as [Z]. destruct (symmetric_point_construction P Z) as [R]. destruct (symmetric_point_construction P' Z) as [R']. assert (Coplanar A B C Z) by (apply bet_cop2__cop with X Y; Between). assert (Cong Z P Z P'). apply per_double_cong with X; Col. apply five_segment with R R' Z Z; Between. apply cong_transitivity with P Z; [|apply cong_transitivity with P' Z]; Cong. apply cong_symmetry, l7_13 with Y; [apply symmetry_preserves_midpoint with P X P' Z|]; assumption. apply per_double_cong with Y; Col. intro; treat_equalities; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2