proposition: Lemma plgs_half_plgs_aux : forall A B C D P Q, Parallelogram_strict A B C D -> Midpoint P A B -> Midpoint Q C D -> Parallelogram_strict A P Q D.
proof: Proof. intros. assert(HH:= H). apply plgs_mid in HH. ex_and HH M. assert(HH:=half_plgs A B C D P Q M H H0 H1 H2). spliter. assert(HH:=H). apply plgs_par_strict in HH. spliter. assert(HH:=par_cong_mid P Q A D H4 (cong_symmetry A D P Q H6)). ex_and HH N. induction H9. spliter. apply False_ind. unfold Par_strict in H7. spliter. apply H11. exists N. assert_diffs; split; ColR. spliter. assert(A <> P). intro. subst P. apply is_midpoint_id in H0. subst B. apply par_strict_distinct in H7. spliter. auto. assert(D <> Q). intro. subst Q. apply l7_2 in H1. apply is_midpoint_id in H1. subst D. apply par_strict_distinct in H7. spliter. auto. eapply mid_plgs. intro. unfold Par_strict in H7. spliter. apply H14. exists Q. split. ColR. Col. apply l7_2. apply H10. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates