proposition: Lemma triangle_mid_par : forall A B C P Q, A <> B -> Midpoint P B C -> Midpoint Q A C -> Par A B Q P.
proof: Proof. intros. elim (col_dec A B C); intro. apply triangle_mid_par_flat with C; auto. apply par_strict_par; apply triangle_mid_par_strict with C; assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec