proposition: Lemma triangle_mid_par_flat_cong_1 : forall A B C P Q R, B <> A -> Col A B C -> Midpoint P B C -> Midpoint Q A C -> Midpoint R A B -> Par A B Q P /\ Cong A R P Q.
proof: Proof. intros. assert (Par A B Q P /\ Cong A R P Q /\ Cong B R P Q) by (apply triangle_mid_par_flat_cong_aux with C; assumption). spliter. split; assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec