proposition: Lemma perp_projp2_eq : forall A A' B B' C D, Projp A A' C D -> Projp B B' C D -> Perp A B C D -> A' = B'.
proof: Proof. intros A A' B B' C D HA' HB' HPerp. destruct HA' as [H HA']; clear H; destruct HB' as [H HB']; clear H. elim HA'; clear HA'; intro HA'; elim HB'; clear HB'; intro HB'. { destruct HA' as [HColA' HA']; destruct HB' as [HColB' HB']. elim (perp_not_col2 A B C D HPerp); intro HNC. { apply l6_21 with A B C D; Col; try (intro; assert_diffs; intuition). { assert (HPar : Par A B A A') by (apply l12_9_2D with C D; Perp). elim HPar; clear HPar; intro HPar; [exfalso; apply HPar; exists A|spliter]; Col. } { assert (HPar : Par A B B B') by (apply l12_9_2D with C D; Perp). elim HPar; clear HPar; intro HPar; [exfalso; apply HPar; exists B|spliter]; Col. } } { apply l6_21 with A B D C; Col; try (intro; assert_diffs; intuition). { assert (HPar : Par A B A A') by (apply l12_9_2D with C D; Perp). elim HPar; clear HPar; intro HPar; [exfalso; apply HPar; exists A|spliter]; Col. } { assert (HPar : Par A B B B') by (apply l12_9_2D with C D; Perp). elim HPar; clear HPar; intro HPar; [exfalso; apply HPar; exists B|spliter]; Col. } } } { destruct HB' as [HColB H]; treat_equalities. apply perp_sym in HPerp; elim (perp_not_col2 C D A B HPerp); intro HNC; [|intuition]; destruct HA' as [HColA' HA']. apply l6_21 with C D A B; Col; try (intro; assert_diffs; intuition). assert (HPar : Par A B A A') by (apply l12_9_2D with C D; Perp). elim HPar; clear HPar; intro HPar; [exfalso; apply HPar; exists A|spliter]; Col. } { destruct HA' as [HColA H]; treat_equalities. apply perp_sym in HPerp; elim (perp_not_col2 C D A B HPerp); intro HNC; [intuition|]; destruct HB' as [HColB' HB']. apply l6_21 with C D B A; Col; try (intro; assert_diffs; intuition). assert (HPar : Par A B B B') by (apply l12_9_2D with C D; Perp). elim HPar; clear HPar; intro HPar; [exfalso; apply HPar; exists B|spliter]; Col. } { spliter; treat_equalities; apply perp_sym in HPerp; elim (perp_not_col2 C D A B HPerp); intuition. } Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors