proposition: Lemma plgs_out_plgs : forall A B C D B' C', Parallelogram_strict A B C D -> Out A B B' -> Out D C C' -> Cong A B' D C' -> Parallelogram_strict A B' C' D.
proof: Proof. intros. assert(OS A D C B /\ OS C B A D). apply plgs_one_side. apply plgs_permut. apply plgs_comm2. assumption. assert( A <> B /\ A <> B' /\ D <> C /\ D <> C'). unfold Out in *. spliter. repeat split; auto. spliter. assert(Par_strict A B C D). apply plgs_par_strict in H. spliter. auto. assert(Par_strict A B' D C'). assert(Par A B' D C'). apply (par_col_par_2 _ B). auto. apply out_col. auto. apply par_symmetry. apply (par_col_par_2 _ C). auto. apply out_col. auto. apply par_symmetry. apply par_right_comm. left. auto. induction H10. auto. spliter. apply False_ind. apply out_col in H0. apply out_col in H1. assert(~Col A C D). intro. apply H9. exists A. split; Col. apply H14. ColR. assert(OS A D B B'). apply (out_one_side_1 A _ _ _ A). intro. apply H9. exists D. split; Col. Col. auto. assert(OS A D C C'). apply (out_one_side_1 _ D _ _ D). intro. apply H9. exists A. split; Col. Col. auto. assert(OS A D B' C'). apply (one_side_transitivity _ _ _ B). apply one_side_symmetry. apply H11. apply (one_side_transitivity _ _ _ C). apply one_side_symmetry. apply H3. assumption. assert(HH:=par_cong_mid_os A B' D C' H10 H2 H13). ex_and HH M. apply (mid_plgs _ _ _ _ M). intro. apply H10. exists C'. split; Col. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec