proposition: Lemma l9_4_1 : forall P Q A C R S M, TS P Q A C -> Col R P Q -> Perp P Q A R -> Col S P Q -> Perp P Q C S -> Midpoint M R S -> (forall U C',Midpoint M U C' -> (Out R U A <-> Out S C C')).
proof: Proof. intros. assert (Le S C R A \/ Le R A S C). apply le_cases. induction H6. apply (l9_4_1_aux P Q A C R S M); assumption. assert((Out R A U <-> Out S C' C) -> (Out R U A <-> Out S C C')). intro. induction H7. split. intro. eapply l6_6. apply H7. apply l6_6. assumption. intro. apply l6_6. apply H8. apply l6_6. assumption. apply H7. assert((Out S C' C <-> Out R A U) -> (Out R A U <-> Out S C' C)). intro. induction H8. split. intro. apply H9. assumption. intro. apply H8. assumption. apply H8. eapply (l9_4_1_aux). assumption. apply l9_2. apply H. assumption. assumption. assumption. assumption. apply l7_2. apply H4. apply l7_2. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar