proposition: Lemma cop_per2__perp : forall A B X Y, A <> B -> X <> Y -> (B <> X \/ B <> Y) -> Coplanar A B X Y -> Per A B X -> Per A B Y -> Perp A B X Y.
proof: Proof. intros. induction H1. assert(HH:=H3). apply per_perp_in in H3; auto. apply perp_in_perp_bis in H3. induction H3. apply perp_not_eq_1 in H3. tauto. apply perp_sym. apply (perp_col _ B); auto. Perp. apply col_permutation_5. apply cop_per2__col with A; Perp; Cop. assert(HH:=H4). apply per_perp_in in H4; auto. apply perp_in_perp_bis in H4. induction H4. apply perp_not_eq_1 in H4. tauto. apply perp_sym. apply perp_left_comm. apply (perp_col _ B); auto. Perp. apply col_permutation_5. eapply cop_per2__col with A; Perp; Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch13_4_cos GeoCoq.Tarski_dev.Annexes.project