proposition: Lemma rect_2_rect : forall A B C1 C2 D1 D2, A <> B -> Rectangle A B C1 D1 -> Rectangle A B C2 D2 -> Rectangle C1 D1 D2 C2.
proof: Proof. intros A B C1 C2 D1 D2 HDiff HRect1 HRect2. elim (eq_dec_points C1 C2); intro HC1C2; treat_equalities. { apply Rectangle_Parallelogram in HRect1; apply plg_mid in HRect1. apply Rectangle_Parallelogram in HRect2; apply plg_mid in HRect2. destruct HRect1 as [M [HMid1 HMid2]]; destruct HRect2 as [M' [HMid3 HMid4]]. treat_equalities; split; Cong; apply parallelogram_to_plg. apply plg_trivial; intro; treat_equalities; auto. } { elim (eq_dec_points B C1); intro HBC1; elim (eq_dec_points B C2); intro HBC2; treat_equalities; [intuition|apply degenerated_rect_eq in HRect1; treat_equalities| apply degenerated_rect_eq in HRect2; treat_equalities|]; apply rect_comm2; auto; apply rect_comm2; do 2 (apply rect_permut); auto. assert (HPara1 := HRect1); apply Rectangle_Parallelogram in HPara1. assert (HPara2 := HRect2); apply Rectangle_Parallelogram in HPara2. assert (HNC1 : ~ Col A B C1) by (apply rect_per2 in HRect1; apply per_not_col; auto). assert (HNC2 : ~ Col A B C2) by (apply rect_per2 in HRect2; apply per_not_col; auto). apply plg_per_rect2. { elim HPara1; clear HPara1; intro HPara1; [|unfold Parallelogram_flat in HPara1; spliter; intuition]. elim HPara2; clear HPara2; intro HPara2; [|unfold Parallelogram_flat in HPara2; spliter; intuition]. apply parallelogram_to_plg; apply plgs_pseudo_trans with B A; apply plgs_comm2; auto; do 2 (apply plgs_permut); auto. } elim (cop_dec A B C1 C2); intro HCop. { apply perp_per_1, perp_sym, cop_par_perp__perp with A B; Cop; apply plg_par_1 in HPara2; Par; clear HPara1; clear HPara2. apply rect_per2 in HRect1; apply rect_per2 in HRect2. assert (HCol : Col C1 C2 B) by (apply cop_per2__col with A; Perp; Cop). apply perp_col0 with B C1; Col; apply per_perp in HRect1; Perp. } { apply rect_per in HRect1; apply rect_per in HRect2; spliter. destruct (eq_dec_points C2 D2); [subst; Perp|]. assert (HOrth : Orth_at C2 B C1 C2 C2 D2); [|destruct HOrth as [_ [_ [_ [_ HOrth]]]]; apply HOrth; Col; Cop]. apply l11_61_bis with B A; Perp; Cop. apply l11_60_bis; Perp; Cop. apply ncop__ncol with A; Cop. } } Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates