proposition: Lemma par_cong3_rect : forall A B C D, A <> C \/ B <> D -> Par A B C D -> Cong A B C D -> Cong A D B C -> Cong A C B D -> Rectangle A B C D \/ Rectangle A B D C.
proof: Proof. intros. unfold Par in H0. induction H0. assert(HH:=par_strict_cong_mid1 A B C D H0 H1). induction HH. spliter. left. unfold Rectangle. split; auto. unfold Plg. split; auto. spliter. ex_and H5 M. right. unfold Rectangle. split; auto. unfold Plg. split; auto. left. intro. subst D. unfold Par_strict in H0. spliter. apply H7. exists A. split; Col. exists M. split; auto. spliter. left. unfold Rectangle. split; auto. apply parallelogram_to_plg. unfold Parallelogram. right. unfold Parallelogram_flat. induction(eq_dec_points C D). subst D. apply cong_identity in H1. subst B. repeat split; Col; Cong. repeat split; Col; Cong; ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates