proposition: Lemma l11_61_bis : forall A B C D E P Q, Orth_at D A B C D P -> Perp D E E Q -> Coplanar A B C E -> Coplanar D E P Q -> Orth_at E A B C E Q.
proof: Proof. intros A B C D E P Q [HNCol [HDP [HD [_ HOrth]]]] HPerp HE HCop. assert_diffs. repeat split; Col. assert (Haux : forall M, Coplanar A B C M -> Per M E Q). { intros M HM. assert (HD' : exists D', Perp D E D' D /\ Coplanar A B C D'). { destruct (ex_ncol_cop A B C D E) as [F []]; auto. destruct (ex_perp_cop D E D F) as [D' []]; auto. exists D'; split; auto. apply coplanar_pseudo_trans with D E F; trivial; apply coplanar_pseudo_trans with A B C; Cop. } destruct HD' as [D' []]. assert_diffs. apply l8_2, (l11_61 D P D'); auto. apply l8_2; Col. Perp. apply coplanar_pseudo_trans with A B C; assumption. Perp. apply l8_2; Col. } intros; apply per_col with Q; Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2