proposition: Lemma triangle_mid_par : forall A B C P Q, ~Col A B C -> Midpoint P B C -> Midpoint Q A C -> Par_strict A B Q P.
proof: Proof. intros. assert(HM:= midpoint_existence A B). ex_and HM R. assert(HH:= l13_1_aux A B C P Q R H H0 H1 H2). ex_and HH X. ex_and H3 Y. assert(Coplanar X Y A P /\ Coplanar X Y A Q /\ Coplanar X Y B P /\ Coplanar X Y B Q). assert(Coplanar A B C A). exists A. left. split; Col. assert(Coplanar A B C B). exists B. left. split; Col. assert(Coplanar A B C P). exists B. left. split; Col. assert(Coplanar A B C Q). exists A. left. split; Col. repeat split; apply coplanar_pseudo_trans with A B C; assumption. spliter. assert(HH:= perp_in_col X Y A B R H3). spliter. apply perp_in_perp_bis in H3. unfold Midpoint in H2. spliter. apply bet_col in H2. assert(X <> Y). apply perp_distinct in H4. tauto. induction H3. assert(Perp Y X A B). apply (perp_col _ R); Perp. Col. apply perp_left_comm in H15. assert(Par A B P Q). apply(l12_9 A B P Q X Y);Perp. induction H16. Par. spliter. assert(Col A B P). ColR. assert(P = B). apply (l6_21 A B C P); Col. unfold Midpoint in H0. spliter. apply bet_col in H0. Col. intro. subst P. contradiction. subst P. unfold Midpoint in H0. spliter. apply cong_symmetry in H21. apply cong_identity in H21. subst C. contradiction. assert(Perp X Y A B). apply (perp_col _ R); Perp. Col. assert(Par A B P Q). apply(l12_9 A B P Q X Y);Perp. induction H16. Par. spliter. assert(Col A B P). ColR. assert(P = B). apply (l6_21 A B C P); Col. unfold Midpoint in H0. spliter. apply bet_col in H0. Col. intro. subst P. contradiction. subst P. unfold Midpoint in H0. spliter. apply cong_symmetry in H21. apply cong_identity in H21. subst C. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel