proposition: Lemma half_plgs : forall A B C D P Q M, Parallelogram_strict A B C D -> Midpoint P A B -> Midpoint Q C D -> Midpoint M A C -> Par P Q A D /\ Midpoint M P Q /\ Cong A D P Q.
proof: Proof. intros. assert(HH:=H). apply plgs_mid in HH. ex_and HH M'. assert(M=M'). eapply l7_17. apply H2. assumption. subst M'. clear H3. prolong P M Q' P M. assert(Midpoint M P Q'). split. assumption. Cong. assert(Midpoint Q' C D). eapply symmetry_preserves_midpoint. apply H2. apply H6. apply H4. apply H0. assert(Q=Q'). eapply l7_17. apply H1. assumption. subst Q'. assert(HH:=H). unfold Parallelogram_strict in HH. spliter. assert(Cong A P D Q). eapply cong_cong_half_1. apply H0. apply l7_2. apply H1. Cong. assert(Par A P Q D). eapply par_col_par_2. intro. subst P. apply is_midpoint_id in H0. subst B. apply par_neq1 in H9. auto. unfold Midpoint in H0. spliter. apply bet_col in H0. apply col_permutation_5. apply H0. apply par_symmetry. apply par_left_comm. eapply par_col_par_2. intro. subst Q. apply cong_identity in H11. subst P. apply is_midpoint_id in H0. subst B. apply par_neq1 in H9. auto. unfold Midpoint in H1. spliter. apply bet_col in H1. apply col_permutation_2. apply H1. apply par_left_comm. Par. assert(Cong A D P Q /\ Par A D P Q). apply(os_cong_par_cong_par A P D Q). unfold TS in H8. assert(~ Col B A C). spliter. assumption. spliter. assert(OS A D P B). eapply out_one_side_1. intro. assert(Col P B D). eapply (col_transitivity_1 _ A). intro. subst P. apply is_midpoint_id in H0. subst B. apply cong_symmetry in H10. apply cong_identity in H10. subst D. apply H14. Col. unfold Midpoint in H0. spliter. apply bet_col in H0. Col. Col. assert(HH:=H). apply plgs_permut in HH. unfold Parallelogram_strict in HH. spliter. unfold TS in H18. assert(~ Col C B D). spliter. assumption. spliter. apply H22. apply col_permutation_1. eapply (col_transitivity_1 _ P). intro. subst P. apply H22. unfold Midpoint in H0. spliter. apply bet_col in H0. Col. Col. Col. Col. unfold Midpoint in H0. spliter. repeat split. intro. subst P. apply cong_symmetry in H11. apply cong_identity in H11; unfold TS in H8. subst Q. apply l7_2 in H1. apply is_midpoint_id in H1. subst D. apply H14. Col. intro. subst B. apply cong_symmetry in H10. apply cong_identity in H10; unfold Par_strict in H12. subst D. apply H13. Col. left. assumption. assert(OS A D Q C). eapply out_one_side_1. intro. apply H14. eapply (col_transitivity_1 _ Q). intro. subst Q. apply l7_2 in H1. apply is_midpoint_id in H1. subst D. apply H14. Col. Col. unfold Midpoint in H1. spliter. apply bet_col in H1. Col. apply col_trivial_2;Col. repeat split. intro. subst Q. apply cong_identity in H11. subst P. unfold OS in H16. ex_and H16 K. unfold TS in H11. spliter. apply H11. Col. intro. subst D. apply cong_identity in H10. subst B. apply H14. Col. unfold Midpoint in H1. spliter. left. Between. assert(OS A D B C). apply ts_cong_par_cong_par in H9. spliter. induction H18. apply l12_6. unfold Par_strict in *. spliter. split; Cop. intro. apply H19. ex_and H20 X. exists X. split; Col. spliter. apply False_ind. apply H13. Col. repeat split; auto. Cong. eapply one_side_transitivity. apply H16. eapply one_side_transitivity. apply H18. apply one_side_symmetry. assumption. assumption. Par. spliter. apply par_symmetry in H14. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates