proposition: Lemma plgf_out_plgf : forall A B C D B' C', Parallelogram_flat A B C D -> Out A B B' -> Out D C C' -> Cong A B' D C' -> Parallelogram_flat A B' C' D.
proof: Proof. intros. assert( A <> B /\ A <> B' /\ D <> C /\ D <> C'). unfold Out in *. spliter. repeat split; auto. spliter. assert(HH:=not_col_exists A B H3). ex_and HH P. assert(HH:=plg_existence A B P H3). ex_and HH Q. assert(Parallelogram_strict A B P Q). induction H8. assumption. unfold Parallelogram_flat in H8. spliter. contradiction. assert(Parallelogram_strict C D Q P). apply(plgf_plgs_trans C D A B P Q). auto. apply plgf_sym. assumption. assumption. assert(HH:=vector_construction A B' Q). ex_and HH P'. induction H11. assert(B <> P). intro. subst P. apply plgs_par_strict in H9. spliter. apply H9. exists B. split; Col. assert(B' <> P'). intro. subst P'. induction H11. apply plgs_par_strict in H11. spliter. apply H11. exists B'. split; Col. unfold Parallelogram_flat in H11. spliter. apply cong_identity in H15. subst Q. apply H9. Col. assert(Col Q P P'). apply plg_par in H8; auto. apply plg_par in H11; auto. spliter. assert(Par A B' P Q). apply (par_col_par_2 _ B). auto. apply out_col. apply H0. assumption. assert(Col P' P Q /\ Col Q P Q). apply(parallel_uniqueness A B' P Q P' Q Q); Col. spliter. Col. assert(Parallelogram_strict A B' P' Q). induction H11. assumption. unfold Parallelogram_flat in H11. spliter. apply False_ind. apply plgs_par_strict in H9. spliter. apply H9. exists Q. split. apply out_col in H0. ColR. Col. assert(P <> Q). intro. subst Q. apply H9. Col. assert(P' <> Q). intro. subst Q. apply H15. Col. assert(Parallelogram_strict D C' P' Q). apply (plgs_out_plgs _ C P). apply plgs_comm2. apply H10. auto. repeat split; auto. unfold Out in H0. spliter. induction H19. left. apply (plgs_plgs_bet A B P Q B' P' H9); auto. right. apply(plgs_plgs_bet A B' P' Q B P); auto. apply plg_cong in H11. spliter. CongR. assert(Parallelogram A B' C' D). apply (plgs_pseudo_trans _ _ P' Q). apply H15. apply plgs_sym. assumption. induction H19. apply False_ind. apply plgs_par_strict in H19. spliter. unfold Parallelogram_flat in H. spliter. apply out_col in H0. apply out_col in H1. apply H19. exists B. split. Col. assert(Col B C D). ColR. ColR. assumption. spliter. subst B'. tauto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec