proposition: Lemma plg_out_plg : forall A B C D B' C', Parallelogram A B C D -> Out A B B' -> Out D C C' -> Cong A B' D C' -> Parallelogram A B' C' D.
proof: Proof. intros. induction H. left. apply (plgs_out_plgs _ B C). apply H. auto. auto. auto. right. apply (plgf_out_plgf _ B C). apply H. auto. auto. auto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec