proposition: Lemma plg_per_rect1 : forall A B C D, Plg A B C D -> Per D A B -> Rectangle A B C D.
proof: Proof. intros. assert(HH:= midpoint_existence A B). ex_and HH P. assert(HH:= midpoint_existence C D). ex_and HH Q. assert(HH:=H). unfold Plg in HH. spliter. ex_and H4 M. apply plg_to_parallelogram in H. induction H. assert(HH:=half_plgs A B C D P Q M H H1 H2 H4). spliter. assert(A <> D /\ P <> Q). apply par_distincts in H6. spliter. split; assumption. spliter. assert(A <> B). intro. subst B. unfold Parallelogram_strict in H. spliter. unfold TS in H. spliter. apply H. Col. assert(A <> P). intro. subst P. apply is_midpoint_id in H1. contradiction. assert(Perp P Q A B). apply (cop_par_perp__perp A D P Q A B). Par. apply per_perp_in in H0. apply perp_in_comm in H0. apply perp_in_perp_bis in H0. induction H0. apply perp_right_comm. assumption. apply perp_not_eq_1 in H0. tauto. auto. assumption. Cop. assert(Perp P M A B). eapply perp_col. intro. subst M. apply is_midpoint_id in H7. contradiction. apply H13. unfold Midpoint in H7. spliter. apply bet_col in H7. Col. assert(Perp A P P M). eapply perp_col. assumption. apply perp_sym. apply H14. unfold Midpoint in H1. spliter. apply bet_col in H1. Col. assert(Per A P M). apply perp_comm in H15. apply perp_perp_in in H15. apply perp_in_comm in H15. apply perp_in_per in H15. assumption. unfold Rectangle. split. apply parallelogram_to_plg . left. assumption. apply l8_2 in H16. unfold Per in H16. ex_and H16 B'. assert(B = B'). eapply symmetric_point_uniqueness. apply H1. assumption. subst B'. unfold Midpoint in H4. spliter. unfold Midpoint in H5. spliter. eapply l2_11. apply H4. apply H5. Cong. apply cong_transitivity with A M; Cong. apply cong_transitivity with B M; Cong. unfold Rectangle. split. apply parallelogram_to_plg. right. assumption. unfold Parallelogram_flat in H. spliter. assert(D = A \/ B = A). apply (l8_9 D A B). assumption. Col. induction H10. subst D. apply cong_symmetry in H8. apply cong_identity in H8. subst C. Cong. subst B. apply cong_symmetry in H7. apply cong_identity in H7. subst D. Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates