proposition: Lemma rect_per1 : forall A B C D, Rectangle A B C D -> Per B A D.
proof: Proof. intros. unfold Rectangle in H. spliter. 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(Per A P Q). eapply (per_col _ _ M). intro. subst M. apply is_midpoint_id in H7. subst Q. apply cong_identity in H8. subst D. assert(B = C). eapply symmetric_point_uniqueness. apply l7_2. apply H5. Midpoint. subst C. unfold Parallelogram_strict in H. spliter. unfold TS in H. spliter. apply H9. Col. apply l8_2. unfold Per. exists B. split. assumption. eapply (cong_cong_half_1 _ M _ _ M) in H0. Cong. assumption. assumption. unfold Midpoint in H7. spliter. apply bet_col. assumption. assert(A <> B). intro. subst B. apply l7_3 in H1. subst P. 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. apply perp_in_per. apply perp_in_comm. apply perp_perp_in. apply perp_sym. apply perp_left_comm. eapply cop_par_perp__perp. apply H6. apply per_perp_in in H9. apply perp_in_perp_bis in H9. induction H9. apply perp_not_eq_1 in H9. tauto. apply perp_sym. eapply perp_col. assumption. apply H9. unfold Midpoint in H1. spliter. apply bet_col. assumption. assumption. apply par_neq1 in H6. assumption. Cop. unfold Parallelogram_flat in H. spliter. assert(A = B /\ C = D \/ A = D /\ C = B). apply(midpoint_cong_uniqueness A C B D M). Col. split; assumption. assumption. induction H10. spliter. subst B. apply l8_2. apply l8_5. spliter. subst D. apply l8_5. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates