proposition: Lemma projp_projp_perp : forall P P1 P2 Q1 Q2, P1 <> P2 -> Projp P1 P Q1 Q2 -> Projp P2 P Q1 Q2 -> Perp P1 P2 Q1 Q2.
proof: Proof. intros P P1 P2 Q1 Q2 HP1P2 H1 H2. destruct H1 as [H H1]; clear H; destruct H2 as [H H2]; clear H. elim H1; clear H1; intro H1; elim H2; clear H2; intro H2; spliter; treat_equalities; Perp; [|intuition]. apply perp_sym; apply perp_col0 with P1 P; Perp; Col. apply col_permutation_2; apply perp2__col with Q1 Q2; Perp. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors