proposition: Lemma triangle_mid_par_strict_cong : forall A B C P Q R, ~Col A B C -> Midpoint P B C -> Midpoint Q A C -> Midpoint R A B -> Par_strict A B Q P /\ Par_strict A C P R /\ Par_strict B C Q R /\ Cong A R P Q /\ Cong B R P Q /\ Cong A Q P R /\ Cong C Q P R /\ Cong B P Q R /\ Cong C P Q R.
proof: Proof. intros. permutation_intro_in_hyps. assert (Par_strict A B Q P /\ Cong A R P Q /\ Cong B R P Q) by (apply triangle_mid_par_strict_cong_aux with C; assumption). assert (Par_strict A C R P /\ Cong A Q P R /\ Cong C Q P R) by (apply triangle_mid_par_strict_cong_aux with B; Col). assert (Par_strict C B Q R /\ Cong C P R Q /\ Cong B P R Q) by (apply triangle_mid_par_strict_cong_aux with A; Col). spliter. split; trivial. split; Par. split; Par. repeat split; Cong. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec