proposition: Lemma col_par_projp2_eq : forall L11 L12 L21 L22 P P' P'', Col L11 L12 P -> Par L11 L12 L21 L22 -> Projp P P' L21 L22 -> Projp P' P'' L11 L12 -> P = P''.
proof: Proof. intros L11 L12 L21 L22 P P' P'' HCol1 HPar HP' HP''. destruct HP' as [HDiff1 HP']; destruct HP'' as [HDiff2 HP'']. elim HP'; clear HP'; intro HP'; elim HP''; clear HP''; intro HP''. { destruct HP' as [HCol2 HPerp1]; destruct HP'' as [HCol3 HPerp2]. assert (H : Par P P' P' P''). { apply l12_9_2D with L11 L12; Perp. apply perp_sym; apply par_perp__perp with L21 L22; Par. } elim H; clear H; intro H; [exfalso; apply H; exists P'; Col|]. destruct H as [HDiff3 [HDiff4 [HCol4 H]]]; clear H. elim (perp_not_col2 L11 L12 P' P'' HPerp2); [intro HNC|intuition]. apply l6_21 with L11 L12 P' P; Col. } { destruct HP' as [HCol2 HPerp1]; destruct HP'' as [HCol3 HPerp2]; treat_equalities. assert (HPerp2 : Perp L11 L12 P' P) by (apply par_perp__perp with L21 L22; Par; Perp). elim (perp_not_col2 L11 L12 P' P HPerp2); [intro HNC|intuition]. apply l6_21 with L11 L12 P' P; Col. } { destruct HP' as [HCol2 HPerp1]; destruct HP'' as [HCol3 HPerp2]; treat_equalities. elim (perp_not_col2 L11 L12 P P'' HPerp2); [intro HNC|intuition]. apply l6_21 with L11 L12 P P''; Col. } { spliter; treat_equalities; auto. } Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors